Metamath Proof Explorer

Theorem xp1st

Description: Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion xp1st 
|- ( A e. ( B X. C ) -> ( 1st ` A ) e. B )

Proof

Step Hyp Ref Expression
1 elxp 
 |-  ( A e. ( B X. C ) <-> E. b E. c ( A = <. b , c >. /\ ( b e. B /\ c e. C ) ) )
2 vex 
 |-  b e. _V
3 vex 
 |-  c e. _V
4 2 3 op1std 
 |-  ( A = <. b , c >. -> ( 1st ` A ) = b )
5 4 eleq1d 
 |-  ( A = <. b , c >. -> ( ( 1st ` A ) e. B <-> b e. B ) )
6 5 biimpar 
 |-  ( ( A = <. b , c >. /\ b e. B ) -> ( 1st ` A ) e. B )
7 6 adantrr 
 |-  ( ( A = <. b , c >. /\ ( b e. B /\ c e. C ) ) -> ( 1st ` A ) e. B )
8 7 exlimivv 
 |-  ( E. b E. c ( A = <. b , c >. /\ ( b e. B /\ c e. C ) ) -> ( 1st ` A ) e. B )
9 1 8 sylbi 
 |-  ( A e. ( B X. C ) -> ( 1st ` A ) e. B )