Metamath Proof Explorer

Theorem altopthc

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

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

Proof

Step Hyp Ref Expression
1 altopthc.1 ⊢ B ∈ V
2 altopthc.2 ⊢ C ∈ V
3 eqcom ⊢ A B = C D ↔ C D = A B
4 2 1 altopthb ⊢ 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