Non-stratified formulas which define sets in New Foundations? As far as I can tell, there are certain non-stratified formulas $\phi(x)$ such that NF proves that $\{x : \phi(x)\}$ exists. For example, fix a set $y$, and let $A = \{x : y \in x\}$ and $B = \{x : x \in y\}$. Then the set $A \cup B = \{x : x \in A \vee x \in B\}$ exists. We have $A \cup B = \{x : x \in y \vee y \in x\}$, so the non-stratified formula $x \in y \vee y \in x$ defines a set.
Can anything be said in general about what classes of non-stratified formulas define sets in NF?
 A: In $NF$ non-stratified formulas can be used in proofs. They are not forbidden like in Russell's Theory of Types. However we can't use non-stratified formulas to prove the existence of sets. In general, if I remember you prove that the sets exist by a different argument, instead of trying to appeal to stratified comprehension which would be hopeless if the formula is non-stratified.
If I am correct, in your example, you have $A \cup B = \{x : x \in y \vee y\in x\}$. You would instead write  $A \cup B = \{x : x \in z \vee y\in x\}$ for $A=\{x : y\in x\}$ and $B=\{x: x\in z\}$, so that you can assign 1 to $y$, 2 to $x$ and 3 to $z$, this is stratified so now the union exists by stratified comprehension. But this does not exclude the case $z=y$ so we have the set  $A \cup B = \{x : x \in y \vee y\in x\}$ even though $x \in y \vee y\in x$ is non-stratified. 
A similar example is done in the book Logical Foundations of Mathematics and Computational Complexity: A Gentle Introduction (Springer Monographs in Mathematics), page 233.
