Theorem elvvuni

Description: An ordered pair contains its union. (Contributed by NM, 16-Sep-2006)

	Ref	Expression
Assertion	elvvuni	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \bigcup A\in A$$

Proof

Step	Hyp	Ref	Expression
1		elvv	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \exists x\exists yA=⟨x,y⟩$$
2		vex	$$⊢x\in \mathrm{V}$$
3		vex	$$⊢y\in \mathrm{V}$$
4	2 3	uniop	$$⊢\bigcup ⟨x,y⟩=\left\{x,y\right\}$$
5	2 3	opi2	$$⊢\left\{x,y\right\}\in ⟨x,y⟩$$
6	4 5	eqeltri	$$⊢\bigcup ⟨x,y⟩\in ⟨x,y⟩$$
7		unieq	$$⊢A=⟨x,y⟩\to \bigcup A=\bigcup ⟨x,y⟩$$
8		id	$$⊢A=⟨x,y⟩\to A=⟨x,y⟩$$
9	7 8	eleq12d	$$⊢A=⟨x,y⟩\to \left(\bigcup A\in A\leftrightarrow \bigcup ⟨x,y⟩\in ⟨x,y⟩\right)$$
10	6 9	mpbiri	$$⊢A=⟨x,y⟩\to \bigcup A\in A$$
11	10	exlimivv	$$⊢\exists x\exists yA=⟨x,y⟩\to \bigcup A\in A$$
12	1 11	sylbi	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \bigcup A\in A$$