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

Metamath Proof Explorer

Theorem preq2b

Description: Biconditional equality lemma for unordered pairs, deduction form. Two unordered pairs have the same first element iff the second elements are equal. (Contributed by AV, 18-Dec-2020)

Ref Expression
Hypotheses preq1b.a ⊢ φ → A ∈ V
preq1b.b ⊢ φ → B ∈ W
Assertion preq2b ⊢ φ → C A = C B ↔ A = B

Proof

Step Hyp Ref Expression
1 preq1b.a ⊢ φ → A ∈ V
2 preq1b.b ⊢ φ → B ∈ W
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 preq1b ⊢ φ → A C = B C ↔ A = B
7 5 6 bitrid ⊢ φ → C A = C B ↔ A = B