How to prove that $\forall x, x\in A\cup B \Leftrightarrow (x\in A\lor x\in B)$ with ZF axioms? I've defined in ZF theory the union of two sets $A$ and $B$ by
$$A\cup B \stackrel{\mathrm{def}}{=} \bigcup \{A, B\}$$
(using the pair and the union axioms)
I want to prove that $\forall x, x\in A\cup B \Leftrightarrow (x\in A\lor x\in B)$ but I don't see how...
Otherwise, how to prove that $\forall x, x\in X \land X=A \Leftrightarrow x\in A$ for example, because I've tried with these axioms some implications like
$$ x \in X \land X\in\{A,B\} \Rightarrow (x\in X \land (X=A \lor X=B)) $$
(I'm using $X\in\{A,B\} \Leftrightarrow (X=A\lor X=B)$ and the tautology $(p\land q)\land (q\Leftrightarrow r) \Rightarrow (p\land r)$ )
Thanks in advance for help.
 A: In one standard formalization of set theory, $X = A$ is an abbreviation for $(\forall z)(z \in X \Leftrightarrow z \in A)$. 
Also, by definition $\{A,B\}$ is defined so that 
$$Q \in \{A,B\} \leftrightarrow (Q = A \lor Q = B).$$
Now, if $z \in \bigcup \{A,B\}$ then there is a $Q \in \{A,B\}$ such that $z \in Q$. Then we have $Q = A \lor Q = B$, so we can deduce $z \in A \lor z \in B$. 
Conversely, if $z \in A \lor z \in B$ then it is easy to prove $z \in \bigcup \{A ,B\}$. 
In other presentations of set theory, where we also include $=$ in the basic language, the equivalence 
$$X = A \Leftrightarrow (\forall z)(z \in X \Leftrightarrow z \in A)$$
is still provable (or may be an axiom), so we can still use the method I just sketched. 
A: Recall the definition of $\bigcup X$: $x\in\bigcup X\iff(\exists Y\in X)(x\in Y)$.
As Carl mentioned, $X=\{A,B\}$ is defined as $\forall Y(Y\in X\leftrightarrow Y=A\lor Y=B)$.
Combining these we get that,
$$x\in A\cup B\iff x\in\bigcup\{A,B\}\iff(\exists Y\in\{A,B\})(x\in Y)\iff x\in A\lor x\in B$$
The first $\iff$ is the definition you wrote; the second is the definition of $\bigcup\{A,B\}$; the last one is due to the definition of $\{A,B\}$ guaranteeing that $Y\in\{A,B\}\iff Y=A\lor Y=B$.
As far as ZF axioms, we used Union to argue that the union is even a set; pairing to argue that $\{A,B\}$ is even a set; and probably extensionality somewhere along the way.
