Theorem wl-mo2tf

Description: Closed form of mof with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 20-Sep-2020)

	Ref	Expression
Assertion	wl-mo2tf	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 Ⅎ 𝑦 𝜑 ) → ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nfnae	⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
2		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 Ⅎ 𝑦 𝜑
3	1 2	nfan	⊢ Ⅎ 𝑥 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 Ⅎ 𝑦 𝜑 )
4		nfnae	⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
5		nfnf1	⊢ Ⅎ 𝑦 Ⅎ 𝑦 𝜑
6	5	nfal	⊢ Ⅎ 𝑦 ∀ 𝑥 Ⅎ 𝑦 𝜑
7	4 6	nfan	⊢ Ⅎ 𝑦 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 Ⅎ 𝑦 𝜑 )
8		simpl	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 Ⅎ 𝑦 𝜑 ) → ¬ ∀ 𝑥 𝑥 = 𝑦 )
9		sp	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → Ⅎ 𝑦 𝜑 )
10	9	adantl	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 Ⅎ 𝑦 𝜑 ) → Ⅎ 𝑦 𝜑 )
11	3 7 8 10	wl-mo2df	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 Ⅎ 𝑦 𝜑 ) → ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) )