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

Metamath Proof Explorer

Theorem preq1b

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

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

Proof

Step Hyp Ref Expression
1 preq1b.a ⊢ φ → A ∈ V
2 preq1b.b ⊢ φ → B ∈ W
3 prid1g ⊢ A ∈ V → A ∈ A C
4 1 3 syl ⊢ φ → A ∈ A C
5 eleq2 ⊢ A C = B C → A ∈ A C ↔ A ∈ B C
6 4 5 syl5ibcom ⊢ φ → A C = B C → A ∈ B C
7 elprg ⊢ A ∈ V → A ∈ B C ↔ A = B ∨ A = C
8 1 7 syl ⊢ φ → A ∈ B C ↔ A = B ∨ A = C
9 6 8 sylibd ⊢ φ → A C = B C → A = B ∨ A = C
10 9 imp ⊢ φ ∧ A C = B C → A = B ∨ A = C
11 prid1g ⊢ B ∈ W → B ∈ B C
12 2 11 syl ⊢ φ → B ∈ B C
13 eleq2 ⊢ A C = B C → B ∈ A C ↔ B ∈ B C
14 12 13 syl5ibrcom ⊢ φ → A C = B C → B ∈ A C
15 elprg ⊢ B ∈ W → B ∈ A C ↔ B = A ∨ B = C
16 2 15 syl ⊢ φ → B ∈ A C ↔ B = A ∨ B = C
17 14 16 sylibd ⊢ φ → A C = B C → B = A ∨ B = C
18 17 imp ⊢ φ ∧ A C = B C → B = A ∨ B = C
19 eqcom ⊢ A = B ↔ B = A
20 eqeq2 ⊢ A = C → B = A ↔ B = C
21 10 18 19 20 oplem1 ⊢ φ ∧ A C = B C → A = B
22 21 ex ⊢ φ → A C = B C → A = B
23 preq1 ⊢ A = B → A C = B C
24 22 23 impbid1 ⊢ φ → A C = B C ↔ A = B