Theorem elvvuni

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

	Ref	Expression
Assertion	elvvuni	|- ( A e. ( _V X. _V ) -> U. A e. A )

Proof

Step	Hyp	Ref	Expression
1		elvv	|- ( A e. ( _V X. _V ) <-> E. x E. y A = <. x , y >. )
2		vex	|- x e. _V
3		vex	|- y e. _V
4	2 3	uniop	|- U. <. x , y >. = { x , y }
5	2 3	opi2	|- { x , y } e. <. x , y >.
6	4 5	eqeltri	|- U. <. x , y >. e. <. x , y >.
7		unieq	|- ( A = <. x , y >. -> U. A = U. <. x , y >. )
8		id	|- ( A = <. x , y >. -> A = <. x , y >. )
9	7 8	eleq12d	|- ( A = <. x , y >. -> ( U. A e. A <-> U. <. x , y >. e. <. x , y >. ) )
10	6 9	mpbiri	|- ( A = <. x , y >. -> U. A e. A )
11	10	exlimivv	|- ( E. x E. y A = <. x , y >. -> U. A e. A )
12	1 11	sylbi	|- ( A e. ( _V X. _V ) -> U. A e. A )