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	$$⊢A\in \left(B\times C\right)\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		elxp6	$$⊢A\in \left(B\times C\right)\leftrightarrow \left(A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\wedge \left(1^{st}\left(A\right)\in B\wedge 2^{nd}\left(A\right)\in C\right)\right)$$
2	1	simplbi	$$⊢A\in \left(B\times C\right)\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$