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

Metamath Proof Explorer

Theorem opelxp

Description: Ordered pair membership in a Cartesian product. (Contributed by NM, 15-Nov-1994) (Proof shortened by Andrew Salmon, 12-Aug-2011) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion opelxp 
|- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )

Proof

Step Hyp Ref Expression
1 elxp2 
 |-  ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2 vex 
 |-  x e. _V
3 vex 
 |-  y e. _V
4 2 3 opth2 
 |-  ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5 eleq1 
 |-  ( A = x -> ( A e. C <-> x e. C ) )
6 eleq1 
 |-  ( B = y -> ( B e. D <-> y e. D ) )
7 5 6 bi2anan9 
 |-  ( ( A = x /\ B = y ) -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
8 4 7 sylbi 
 |-  ( <. A , B >. = <. x , y >. -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
9 8 biimprcd 
 |-  ( ( x e. C /\ y e. D ) -> ( <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) ) )
10 9 rexlimivv 
 |-  ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11 eqid 
 |-  <. A , B >. = <. A , B >.
12 opeq1 
 |-  ( x = A -> <. x , y >. = <. A , y >. )
13 12 eqeq2d 
 |-  ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14 opeq2 
 |-  ( y = B -> <. A , y >. = <. A , B >. )
15 14 eqeq2d 
 |-  ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16 13 15 rspc2ev 
 |-  ( ( A e. C /\ B e. D /\ <. A , B >. = <. A , B >. ) -> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
17 11 16 mp3an3 
 |-  ( ( A e. C /\ B e. D ) -> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
18 10 17 impbii 
 |-  ( E. x e. C E. y e. D <. A , B >. = <. x , y >. <-> ( A e. C /\ B e. D ) )
19 1 18 bitri 
 |-  ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )