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	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		elxp6	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ ∧ ( ( 1st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2nd ‘ 𝐴 ) ∈ 𝐶 ) ) )
2	1	simplbi	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )