xpopth

Description: An ordered pair theorem for members of Cartesian products. (Contributed by NM, 20-Jun-2007)

		Ref	Expression
	Assertion	xpopth	⊢ ( ( 𝐴 ∈ ( 𝐶 × 𝐷 ) ∧ 𝐵 ∈ ( 𝑅 × 𝑆 ) ) → ( ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) ↔ 𝐴 = 𝐵 ) )

Step	Hyp	Ref	Expression
1		1st2nd2	⊢ ( 𝐴 ∈ ( 𝐶 × 𝐷 ) → 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ )
2		1st2nd2	⊢ ( 𝐵 ∈ ( 𝑅 × 𝑆 ) → 𝐵 = ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ )
3	1 2	eqeqan12d	⊢ ( ( 𝐴 ∈ ( 𝐶 × 𝐷 ) ∧ 𝐵 ∈ ( 𝑅 × 𝑆 ) ) → ( 𝐴 = 𝐵 ↔ ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ = ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ ) )
4		fvex	⊢ ( 1^st ‘ 𝐴 ) ∈ V
5		fvex	⊢ ( 2^nd ‘ 𝐴 ) ∈ V
6	4 5	opth	⊢ ( ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ = ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ ↔ ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) )
7	3 6	bitr2di	⊢ ( ( 𝐴 ∈ ( 𝐶 × 𝐷 ) ∧ 𝐵 ∈ ( 𝑅 × 𝑆 ) ) → ( ( ( 1^st ‘ 𝐴 ) = ( 1^st ‘ 𝐵 ) ∧ ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ 𝐵 ) ) ↔ 𝐴 = 𝐵 ) )

Metamath Proof Explorer