Theorem opthg2

Description: Ordered pair theorem. (Contributed by NM, 14-Oct-2005) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	opthg2	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		opthg	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) → ( ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) ) )
2		eqcom	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
3		eqcom	⊢ ( 𝐴 = 𝐶 ↔ 𝐶 = 𝐴 )
4		eqcom	⊢ ( 𝐵 = 𝐷 ↔ 𝐷 = 𝐵 )
5	3 4	anbi12i	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ↔ ( 𝐶 = 𝐴 ∧ 𝐷 = 𝐵 ) )
6	1 2 5	3bitr4g	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )