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 ⊢φ→AC=BC↔A=B

Proof

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