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

Metamath Proof Explorer

Theorem opeqpr

Description: Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008) (Avoid depending on this detail.)

Ref Expression
Hypotheses opeqpr.1 ⊢ 𝐴 ∈ V
opeqpr.2 ⊢ 𝐵 ∈ V
opeqpr.3 ⊢ 𝐶 ∈ V
opeqpr.4 ⊢ 𝐷 ∈ V
Assertion opeqpr ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐶 , 𝐷 } ↔ ( ( 𝐶 = { 𝐴 } ∧ 𝐷 = { 𝐴 , 𝐵 } ) ∨ ( 𝐶 = { 𝐴 , 𝐵 } ∧ 𝐷 = { 𝐴 } ) ) )

Proof

Step Hyp Ref Expression
1 opeqpr.1 ⊢ 𝐴 ∈ V
2 opeqpr.2 ⊢ 𝐵 ∈ V
3 opeqpr.3 ⊢ 𝐶 ∈ V
4 opeqpr.4 ⊢ 𝐷 ∈ V
5 eqcom ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐶 , 𝐷 } ↔ { 𝐶 , 𝐷 } = ⟨ 𝐴 , 𝐵 ⟩ )
6 1 2 dfop ⊢ ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } }
7 6 eqeq2i ⊢ ( { 𝐶 , 𝐷 } = ⟨ 𝐴 , 𝐵 ⟩ ↔ { 𝐶 , 𝐷 } = { { 𝐴 } , { 𝐴 , 𝐵 } } )
8 snex ⊢ { 𝐴 } ∈ V
9 prex ⊢ { 𝐴 , 𝐵 } ∈ V
10 3 4 8 9 preq12b ⊢ ( { 𝐶 , 𝐷 } = { { 𝐴 } , { 𝐴 , 𝐵 } } ↔ ( ( 𝐶 = { 𝐴 } ∧ 𝐷 = { 𝐴 , 𝐵 } ) ∨ ( 𝐶 = { 𝐴 , 𝐵 } ∧ 𝐷 = { 𝐴 } ) ) )
11 5 7 10 3bitri ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐶 , 𝐷 } ↔ ( ( 𝐶 = { 𝐴 } ∧ 𝐷 = { 𝐴 , 𝐵 } ) ∨ ( 𝐶 = { 𝐴 , 𝐵 } ∧ 𝐷 = { 𝐴 } ) ) )