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

Metamath Proof Explorer

Theorem preqr2

Description: Reverse equality lemma for unordered pairs. If two unordered pairs have the same first element, the second elements are equal. (Contributed by NM, 15-Jul-1993)

Ref Expression
Hypotheses preqr1.a ⊢ A ∈ V
preqr1.b ⊢ B ∈ V
Assertion preqr2 ⊢ C A = C B → A = B

Proof

Step Hyp Ref Expression
1 preqr1.a ⊢ A ∈ V
2 preqr1.b ⊢ B ∈ V
3 prcom ⊢ C A = A C
4 prcom ⊢ C B = B C
5 3 4 eqeq12i ⊢ C A = C B ↔ A C = B C
6 1 2 preqr1 ⊢ A C = B C → A = B
7 5 6 sylbi ⊢ C A = C B → A = B