This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ V
preqr1.b ⊢ 𝐵 ∈ V
preq12b.c ⊢ 𝐶 ∈ V
preq12b.d ⊢ 𝐷 ∈ V
Assertion opthpr ( 𝐴 ≠ 𝐷 → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 preqr1.a ⊢ 𝐴 ∈ V
2 preqr1.b ⊢ 𝐵 ∈ V
3 preq12b.c ⊢ 𝐶 ∈ V
4 preq12b.d ⊢ 𝐷 ∈ V
5 1 2 3 4 preq12b ⊢ ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) )
6 idd ⊢ ( 𝐴 ≠ 𝐷 → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
7 df-ne ⊢ ( 𝐴 ≠ 𝐷 ↔ ¬ 𝐴 = 𝐷 )
8 pm2.21 ⊢ ( ¬ 𝐴 = 𝐷 → ( 𝐴 = 𝐷 → ( 𝐵 = 𝐶 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) )
9 7 8 sylbi ⊢ ( 𝐴 ≠ 𝐷 → ( 𝐴 = 𝐷 → ( 𝐵 = 𝐶 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) )
10 9 impd ⊢ ( 𝐴 ≠ 𝐷 → ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
11 6 10 jaod ⊢ ( 𝐴 ≠ 𝐷 → ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
12 orc ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) )
13 11 12 impbid1 ⊢ ( 𝐴 ≠ 𝐷 → ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
14 5 13 bitrid ⊢ ( 𝐴 ≠ 𝐷 → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )