Metamath Proof Explorer


Theorem wl-mo2df

Description: Version of mof 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, 11-Aug-2019)

Ref Expression
Hypotheses wl-mo2df.1 𝑥 𝜑
wl-mo2df.2 𝑦 𝜑
wl-mo2df.3 ( 𝜑 → ¬ ∀ 𝑥 𝑥 = 𝑦 )
wl-mo2df.4 ( 𝜑 → Ⅎ 𝑦 𝜓 )
Assertion wl-mo2df ( 𝜑 → ( ∃* 𝑥 𝜓 ↔ ∃ 𝑦𝑥 ( 𝜓𝑥 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 wl-mo2df.1 𝑥 𝜑
2 wl-mo2df.2 𝑦 𝜑
3 wl-mo2df.3 ( 𝜑 → ¬ ∀ 𝑥 𝑥 = 𝑦 )
4 wl-mo2df.4 ( 𝜑 → Ⅎ 𝑦 𝜓 )
5 df-mo ( ∃* 𝑥 𝜓 ↔ ∃ 𝑢𝑥 ( 𝜓𝑥 = 𝑢 ) )
6 nfeqf1 ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑦 𝑥 = 𝑢 )
7 6 naecoms ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 = 𝑢 )
8 3 7 syl ( 𝜑 → Ⅎ 𝑦 𝑥 = 𝑢 )
9 4 8 nfimd ( 𝜑 → Ⅎ 𝑦 ( 𝜓𝑥 = 𝑢 ) )
10 1 9 nfald ( 𝜑 → Ⅎ 𝑦𝑥 ( 𝜓𝑥 = 𝑢 ) )
11 nfnae 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
12 nfeqf2 ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑢 = 𝑦 )
13 11 12 nfan1 𝑥 ( ¬ ∀ 𝑥 𝑥 = 𝑦𝑢 = 𝑦 )
14 equequ2 ( 𝑢 = 𝑦 → ( 𝑥 = 𝑢𝑥 = 𝑦 ) )
15 14 imbi2d ( 𝑢 = 𝑦 → ( ( 𝜓𝑥 = 𝑢 ) ↔ ( 𝜓𝑥 = 𝑦 ) ) )
16 15 adantl ( ( ¬ ∀ 𝑥 𝑥 = 𝑦𝑢 = 𝑦 ) → ( ( 𝜓𝑥 = 𝑢 ) ↔ ( 𝜓𝑥 = 𝑦 ) ) )
17 13 16 albid ( ( ¬ ∀ 𝑥 𝑥 = 𝑦𝑢 = 𝑦 ) → ( ∀ 𝑥 ( 𝜓𝑥 = 𝑢 ) ↔ ∀ 𝑥 ( 𝜓𝑥 = 𝑦 ) ) )
18 3 17 sylan ( ( 𝜑𝑢 = 𝑦 ) → ( ∀ 𝑥 ( 𝜓𝑥 = 𝑢 ) ↔ ∀ 𝑥 ( 𝜓𝑥 = 𝑦 ) ) )
19 18 ex ( 𝜑 → ( 𝑢 = 𝑦 → ( ∀ 𝑥 ( 𝜓𝑥 = 𝑢 ) ↔ ∀ 𝑥 ( 𝜓𝑥 = 𝑦 ) ) ) )
20 2 10 19 cbvexd ( 𝜑 → ( ∃ 𝑢𝑥 ( 𝜓𝑥 = 𝑢 ) ↔ ∃ 𝑦𝑥 ( 𝜓𝑥 = 𝑦 ) ) )
21 5 20 syl5bb ( 𝜑 → ( ∃* 𝑥 𝜓 ↔ ∃ 𝑦𝑥 ( 𝜓𝑥 = 𝑦 ) ) )