Metamath Proof Explorer

Theorem xpopth

Description: An ordered pair theorem for members of Cartesian products. (Contributed by NM, 20-Jun-2007)

Ref Expression
Assertion xpopth 
|- ( ( A e. ( C X. D ) /\ B e. ( R X. S ) ) -> ( ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 1st2nd2 
 |-  ( A e. ( C X. D ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
2 1st2nd2 
 |-  ( B e. ( R X. S ) -> B = <. ( 1st ` B ) , ( 2nd ` B ) >. )
3 1 2 eqeqan12d 
 |-  ( ( A e. ( C X. D ) /\ B e. ( R X. S ) ) -> ( A = B <-> <. ( 1st ` A ) , ( 2nd ` A ) >. = <. ( 1st ` B ) , ( 2nd ` B ) >. ) )
4 fvex 
 |-  ( 1st ` A ) e. _V
5 fvex 
 |-  ( 2nd ` A ) e. _V
6 4 5 opth 
 |-  ( <. ( 1st ` A ) , ( 2nd ` A ) >. = <. ( 1st ` B ) , ( 2nd ` B ) >. <-> ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) )
7 3 6 bitr2di 
 |-  ( ( A e. ( C X. D ) /\ B e. ( R X. S ) ) -> ( ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) <-> A = B ) )