Metamath Proof Explorer


Theorem 1st2nd2

Description: Reconstruction of a member of a Cartesian product in terms of its ordered pair components. (Contributed by NM, 20-Oct-2013)

Ref Expression
Assertion 1st2nd2 AB×CA=1stA2ndA

Proof

Step Hyp Ref Expression
1 elxp6 AB×CA=1stA2ndA1stAB2ndAC
2 1 simplbi AB×CA=1stA2ndA