Metamath Proof Explorer

Theorem elxp8

Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp7 . (Contributed by ML, 19-Oct-2020)

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

Proof

Step Hyp Ref Expression
1 xp1st 
 |-  ( A e. ( B X. C ) -> ( 1st ` A ) e. B )
2 ssv 
 |-  B C_ _V
3 ssid 
 |-  C C_ C
4 xpss12 
 |-  ( ( B C_ _V /\ C C_ C ) -> ( B X. C ) C_ ( _V X. C ) )
5 2 3 4 mp2an 
 |-  ( B X. C ) C_ ( _V X. C )
6 5 sseli 
 |-  ( A e. ( B X. C ) -> A e. ( _V X. C ) )
7 1 6 jca 
 |-  ( A e. ( B X. C ) -> ( ( 1st ` A ) e. B /\ A e. ( _V X. C ) ) )
8 xpss 
 |-  ( _V X. C ) C_ ( _V X. _V )
9 8 sseli 
 |-  ( A e. ( _V X. C ) -> A e. ( _V X. _V ) )
10 9 adantl 
 |-  ( ( ( 1st ` A ) e. B /\ A e. ( _V X. C ) ) -> A e. ( _V X. _V ) )
11 xp2nd 
 |-  ( A e. ( _V X. C ) -> ( 2nd ` A ) e. C )
12 11 anim2i 
 |-  ( ( ( 1st ` A ) e. B /\ A e. ( _V X. C ) ) -> ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) )
13 elxp7 
 |-  ( A e. ( B X. C ) <-> ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. B /\ ( 2nd ` A ) e. C ) ) )
14 10 12 13 sylanbrc 
 |-  ( ( ( 1st ` A ) e. B /\ A e. ( _V X. C ) ) -> A e. ( B X. C ) )
15 7 14 impbii 
 |-  ( A e. ( B X. C ) <-> ( ( 1st ` A ) e. B /\ A e. ( _V X. C ) ) )