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 B × C 1 st A B

Proof

Step Hyp Ref Expression
1 elxp A B × C b c A = b c b B c C
2 vex b V
3 vex c V
4 2 3 op1std A = b c 1 st A = b
5 4 eleq1d A = b c 1 st A B b B
6 5 biimpar A = b c b B 1 st A B
7 6 adantrr A = b c b B c C 1 st A B
8 7 exlimivv b c A = b c b B c C 1 st A B
9 1 8 sylbi A B × C 1 st A B