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

Metamath Proof Explorer

Theorem opeluu

Description: Each member of an ordered pair belongs to the union of the union of a class to which the ordered pair belongs. Lemma 3D of Enderton p. 41. (Contributed by NM, 31-Mar-1995) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses opeluu.1 
|- A e. _V
opeluu.2 
|- B e. _V
Assertion opeluu 
|- ( <. A , B >. e. C -> ( A e. U. U. C /\ B e. U. U. C ) )

Proof

Step Hyp Ref Expression
1 opeluu.1 
 |-  A e. _V
2 opeluu.2 
 |-  B e. _V
3 1 prid1 
 |-  A e. { A , B }
4 1 2 opi2 
 |-  { A , B } e. <. A , B >.
5 elunii 
 |-  ( ( { A , B } e. <. A , B >. /\ <. A , B >. e. C ) -> { A , B } e. U. C )
6 4 5 mpan 
 |-  ( <. A , B >. e. C -> { A , B } e. U. C )
7 elunii 
 |-  ( ( A e. { A , B } /\ { A , B } e. U. C ) -> A e. U. U. C )
8 3 6 7 sylancr 
 |-  ( <. A , B >. e. C -> A e. U. U. C )
9 2 prid2 
 |-  B e. { A , B }
10 elunii 
 |-  ( ( B e. { A , B } /\ { A , B } e. U. C ) -> B e. U. U. C )
11 9 6 10 sylancr 
 |-  ( <. A , B >. e. C -> B e. U. U. C )
12 8 11 jca 
 |-  ( <. A , B >. e. C -> ( A e. U. U. C /\ B e. U. U. C ) )