Theorem opth2

Description: Ordered pair theorem. (Contributed by NM, 21-Sep-2014)

	Ref	Expression
Hypotheses	opth2.1	⊢ 𝐶 ∈ V
	opth2.2	⊢ 𝐷 ∈ V
Assertion	opth2	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		opth2.1	⊢ 𝐶 ∈ V
2		opth2.2	⊢ 𝐷 ∈ V
3		opthg2	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
4	1 2 3	mp2an	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )