Metamath Proof Explorer

Theorem elxp7

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

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

Proof

Step Hyp Ref Expression
1 elxp6 
 |-  ( A e. ( B X. C ) <-> ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )
2 fvex 
 |-  ( 1st ` A ) e. _V
3 fvex 
 |-  ( 2nd ` A ) e. _V
4 2 3 pm3.2i 
 |-  ( ( 1st ` A ) e. _V /\ ( 2nd ` A ) e. _V )
5 elxp6 
 |-  ( A e. ( _V X. _V ) <-> ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. _V /\ ( 2nd ` A ) e. _V ) ) )
6 4 5 mpbiran2 
 |-  ( A e. ( _V X. _V ) <-> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
7 6 anbi1i 
 |-  ( ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) <-> ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )
8 1 7 bitr4i 
 |-  ( A e. ( B X. C ) <-> ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )