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 ⊢ φ → Ⅎ y x = z
7 3 6 nfbid ⊢ φ → Ⅎ y ψ ↔ x = z
8 nfvd ⊢ φ → Ⅎ x y = 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 χ