Metamath Proof Explorer

Theorem opth2

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

Ref Expression
Hypotheses opth2.1 ⊢ C ∈ V
opth2.2 ⊢ D ∈ V
Assertion opth2 ⊢ A B = C D ↔ A = C ∧ B = D

Proof

Step Hyp Ref Expression
1 opth2.1 ⊢ C ∈ V
2 opth2.2 ⊢ D ∈ V
3 opthg2 ⊢ C ∈ V ∧ D ∈ V → A B = C D ↔ A = C ∧ B = D
4 1 2 3 mp2an ⊢ A B = C D ↔ A = C ∧ B = D