This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opthg2

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

Ref Expression
Assertion opthg2 ⊢ C ∈ V ∧ D ∈ W → A B = C D ↔ A = C ∧ B = D

Proof

Step Hyp Ref Expression
1 opthg ⊢ C ∈ V ∧ D ∈ W → C D = A B ↔ C = A ∧ D = B
2 eqcom ⊢ A B = C D ↔ C D = A B
3 eqcom ⊢ A = C ↔ C = A
4 eqcom ⊢ B = D ↔ D = B
5 3 4 anbi12i ⊢ A = C ∧ B = D ↔ C = A ∧ D = B
6 1 2 5 3bitr4g ⊢ C ∈ V ∧ D ∈ W → A B = C D ↔ A = C ∧ B = D