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

Metamath Proof Explorer

Theorem opthg

Description: Ordered pair theorem. C and D are not required to be sets under our specific ordered pair definition. (Contributed by NM, 14-Oct-2005) (Revised by Mario Carneiro, 26-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 opeq1 ⊢ x = A → x y = A y
2 1 eqeq1d ⊢ x = A → x y = C D ↔ A y = C D
3 eqeq1 ⊢ x = A → x = C ↔ A = C
4 3 anbi1d ⊢ x = A → x = C ∧ y = D ↔ A = C ∧ y = D
5 2 4 bibi12d ⊢ x = A → x y = C D ↔ x = C ∧ y = D ↔ A y = C D ↔ A = C ∧ y = D
6 opeq2 ⊢ y = B → A y = A B
7 6 eqeq1d ⊢ y = B → A y = C D ↔ A B = C D
8 eqeq1 ⊢ y = B → y = D ↔ B = D
9 8 anbi2d ⊢ y = B → A = C ∧ y = D ↔ A = C ∧ B = D
10 7 9 bibi12d ⊢ y = B → A y = C D ↔ A = C ∧ y = D ↔ A B = C D ↔ A = C ∧ B = D
11 vex ⊢ x ∈ V
12 vex ⊢ y ∈ V
13 11 12 opth ⊢ x y = C D ↔ x = C ∧ y = D
14 5 10 13 vtocl2g ⊢ A ∈ V ∧ B ∈ W → A B = C D ↔ A = C ∧ B = D