Metamath Proof Explorer

Theorem wl-eudf

Description: Version of eu6 with a context and a distinctor replacing a distinct variable condition. This version should be used only to eliminate disjoint variable conditions. (Contributed by Wolf Lammen, 23-Sep-2020)

Ref Expression
Hypotheses wl-eudf.1 ⊢ Ⅎ x φ
wl-eudf.2 ⊢ Ⅎ y φ
wl-eudf.3 ⊢ φ → ¬ ∀ x x = y
wl-eudf.4 ⊢ φ → Ⅎ y ψ
Assertion wl-eudf ⊢ φ → ∃! x ψ ↔ ∃ y ∀ x ψ ↔ x = y

Proof

Step Hyp Ref Expression
1 wl-eudf.1 ⊢ Ⅎ x φ
2 wl-eudf.2 ⊢ Ⅎ y φ
3 wl-eudf.3 ⊢ φ → ¬ ∀ x x = y
4 wl-eudf.4 ⊢ φ → Ⅎ y ψ
5 eu6 ⊢ ∃! x ψ ↔ ∃ u ∀ x ψ ↔ x = u
6 nfeqf1 ⊢ ¬ ∀ y y = x → Ⅎ y x = u
7 6 naecoms ⊢ ¬ ∀ x x = y → Ⅎ y x = u
8 3 7 syl ⊢ φ → Ⅎ y x = u
9 4 8 nfbid ⊢ φ → Ⅎ y ψ ↔ x = u
10 1 9 nfald ⊢ φ → Ⅎ y ∀ x ψ ↔ x = u
11 nfnae ⊢ Ⅎ x ¬ ∀ x x = y
12 nfeqf2 ⊢ ¬ ∀ x x = y → Ⅎ x u = y
13 11 12 nfan1 ⊢ Ⅎ x ¬ ∀ x x = y ∧ u = y
14 equequ2 ⊢ u = y → x = u ↔ x = y
15 14 bibi2d ⊢ u = y → ψ ↔ x = u ↔ ψ ↔ x = y
16 15 adantl ⊢ ¬ ∀ x x = y ∧ u = y → ψ ↔ x = u ↔ ψ ↔ x = y
17 13 16 albid ⊢ ¬ ∀ x x = y ∧ u = y → ∀ x ψ ↔ x = u ↔ ∀ x ψ ↔ x = y
18 3 17 sylan ⊢ φ ∧ u = y → ∀ x ψ ↔ x = u ↔ ∀ x ψ ↔ x = y
19 18 ex ⊢ φ → u = y → ∀ x ψ ↔ x = u ↔ ∀ x ψ ↔ x = y
20 2 10 19 cbvexd ⊢ φ → ∃ u ∀ x ψ ↔ x = u ↔ ∃ y ∀ x ψ ↔ x = y
21 5 20 bitrid ⊢ φ → ∃! x ψ ↔ ∃ y ∀ x ψ ↔ x = y