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

Metamath Proof Explorer

Theorem elxp6

Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 . (Contributed by NM, 9-Oct-2004)

Ref Expression
Assertion elxp6 
|- ( A e. ( B X. C ) <-> ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )

Proof

Step Hyp Ref Expression
1 elxp4 
 |-  ( A e. ( B X. C ) <-> ( A = <. U. dom { A } , U. ran { A } >. /\ ( U. dom { A } e. B /\ U. ran { A } e. C ) ) )
2 1stval 
 |-  ( 1st ` A ) = U. dom { A }
3 2ndval 
 |-  ( 2nd ` A ) = U. ran { A }
4 2 3 opeq12i 
 |-  <. ( 1st ` A ) , ( 2nd ` A ) >. = <. U. dom { A } , U. ran { A } >.
5 4 eqeq2i 
 |-  ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. <-> A = <. U. dom { A } , U. ran { A } >. )
6 2 eleq1i 
 |-  ( ( 1st ` A ) e. B <-> U. dom { A } e. B )
7 3 eleq1i 
 |-  ( ( 2nd ` A ) e. C <-> U. ran { A } e. C )
8 6 7 anbi12i 
 |-  ( ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) <-> ( U. dom { A } e. B /\ U. ran { A } e. C ) )
9 5 8 anbi12i 
 |-  ( ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) <-> ( A = <. U. dom { A } , U. ran { A } >. /\ ( U. dom { A } e. B /\ U. ran { A } e. C ) ) )
10 1 9 bitr4i 
 |-  ( A e. ( B X. C ) <-> ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )