Metamath Proof Explorer

Theorem opthpr

Description: An unordered pair has the ordered pair property (compare opth ) under certain conditions. (Contributed by NM, 27-Mar-2007)

Ref Expression
Hypotheses preqr1.a ⊢ A ∈ V
preqr1.b ⊢ B ∈ V
preq12b.c ⊢ C ∈ V
preq12b.d ⊢ D ∈ V
Assertion opthpr ⊢ A ≠ D → A B = C D ↔ A = C ∧ B = D

Proof

Step Hyp Ref Expression
1 preqr1.a ⊢ A ∈ V
2 preqr1.b ⊢ B ∈ V
3 preq12b.c ⊢ C ∈ V
4 preq12b.d ⊢ D ∈ V
5 1 2 3 4 preq12b ⊢ A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
6 idd ⊢ A ≠ D → A = C ∧ B = D → A = C ∧ B = D
7 df-ne ⊢ A ≠ D ↔ ¬ A = D
8 pm2.21 ⊢ ¬ A = D → A = D → B = C → A = C ∧ B = D
9 7 8 sylbi ⊢ A ≠ D → A = D → B = C → A = C ∧ B = D
10 9 impd ⊢ A ≠ D → A = D ∧ B = C → A = C ∧ B = D
11 6 10 jaod ⊢ A ≠ D → A = C ∧ B = D ∨ A = D ∧ B = C → A = C ∧ B = D
12 orc ⊢ A = C ∧ B = D → A = C ∧ B = D ∨ A = D ∧ B = C
13 11 12 impbid1 ⊢ A ≠ D → A = C ∧ B = D ∨ A = D ∧ B = C ↔ A = C ∧ B = D
14 5 13 bitrid ⊢ A ≠ D → A B = C D ↔ A = C ∧ B = D