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

Metamath Proof Explorer

Theorem preqr1

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

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

Proof

Step Hyp Ref Expression
1 preqr1.a ⊢ A ∈ V
2 preqr1.b ⊢ B ∈ V
3 id ⊢ A ∈ V → A ∈ V
4 2 a1i ⊢ A ∈ V → B ∈ V
5 3 4 preq1b ⊢ A ∈ V → A C = B C ↔ A = B
6 1 5 ax-mp ⊢ A C = B C ↔ A = B
7 6 biimpi ⊢ A C = B C → A = B