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	⊢ ( 𝜑 → ( ∃* 𝑥 𝜓 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜓 → 𝑥 = 𝑦 ) ) )