Metamath Proof Explorer

Theorem cbveud

Description: Deduction used to change bound variables in an existential uniqueness quantifier, using implicit substitution. (Contributed by ML, 27-Mar-2021)

Ref Expression
Hypotheses cbveud.1 ⊢Ⅎxφ
cbveud.2 ⊢Ⅎyφ
cbveud.3 ⊢φ→Ⅎyψ
cbveud.4 ⊢φ→Ⅎxχ
cbveud.5 ⊢φ→x=y→ψ↔χ
Assertion cbveud ⊢φ→∃!xψ↔∃!yχ

Proof

Step Hyp Ref Expression
1 cbveud.1 ⊢Ⅎxφ
2 cbveud.2 ⊢Ⅎyφ
3 cbveud.3 ⊢φ→Ⅎyψ
4 cbveud.4 ⊢φ→Ⅎxχ
5 cbveud.5 ⊢φ→x=y→ψ↔χ
6 nfvd ⊢φ→Ⅎyx=z
7 3 6 nfbid ⊢φ→Ⅎyψ↔x=z
8 nfvd ⊢φ→Ⅎxy=z
9 4 8 nfbid ⊢φ→Ⅎxχ↔y=z
10 simpr ⊢x=y∧ψ↔χ→ψ↔χ
11 equequ1 ⊢x=y→x=z↔y=z
12 11 adantr ⊢x=y∧ψ↔χ→x=z↔y=z
13 10 12 bibi12d ⊢x=y∧ψ↔χ→ψ↔x=z↔χ↔y=z
14 13 ex ⊢x=y→ψ↔χ→ψ↔x=z↔χ↔y=z
15 5 14 sylcom ⊢φ→x=y→ψ↔x=z↔χ↔y=z
16 1 2 7 9 15 cbv2w ⊢φ→∀xψ↔x=z↔∀yχ↔y=z
17 16 exbidv ⊢φ→∃z∀xψ↔x=z↔∃z∀yχ↔y=z
18 eu6 ⊢∃!xψ↔∃z∀xψ↔x=z
19 eu6 ⊢∃!yχ↔∃z∀yχ↔y=z
20 17 18 19 3bitr4g ⊢φ→∃!xψ↔∃!yχ