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 ⊢ A ∈ V
opeqpr.2 ⊢ B ∈ V
opeqpr.3 ⊢ C ∈ V
opeqpr.4 ⊢ D ∈ V
Assertion opeqpr ⊢ A B = C D ↔ C = A ∧ D = A B ∨ C = A B ∧ D = A

Proof

Step Hyp Ref Expression
1 opeqpr.1 ⊢ A ∈ V
2 opeqpr.2 ⊢ B ∈ V
3 opeqpr.3 ⊢ C ∈ V
4 opeqpr.4 ⊢ D ∈ V
5 eqcom ⊢ A B = C D ↔ C D = A B
6 1 2 dfop ⊢ A B = A A B
7 6 eqeq2i ⊢ C D = A B ↔ C D = A A B
8 snex ⊢ A ∈ V
9 prex ⊢ A B ∈ V
10 3 4 8 9 preq12b ⊢ C D = A A B ↔ C = A ∧ D = A B ∨ C = A B ∧ D = A
11 5 7 10 3bitri ⊢ A B = C D ↔ C = A ∧ D = A B ∨ C = A B ∧ D = A