This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )