Metamath Proof Explorer

Theorem altopthd

Description: Alternate ordered pair theorem with different sethood requirements. See altopth for more comments. (Contributed by Scott Fenton, 14-Apr-2012)

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

Proof

Step Hyp Ref Expression
1 altopthd.1 ⊢ C ∈ V
2 altopthd.2 ⊢ D ∈ V
3 eqcom ⊢ A B = C D ↔ C D = A B
4 1 2 altopth ⊢ C D = A B ↔ C = A ∧ D = B
5 eqcom ⊢ C = A ↔ A = C
6 eqcom ⊢ D = B ↔ B = D
7 5 6 anbi12i ⊢ C = A ∧ D = B ↔ A = C ∧ B = D
8 3 4 7 3bitri ⊢ A B = C D ↔ A = C ∧ B = D