Metamath Proof Explorer

Theorem altopthb

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

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

Proof

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