Theorem wl-mo2t

Description: Closed form of mof . (Contributed by Wolf Lammen, 18-Aug-2019)

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

Proof

Step	Hyp	Ref	Expression
1		dfmo	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑢 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑢 ) )
2		nfnf1	⊢ Ⅎ 𝑦 Ⅎ 𝑦 𝜑
3	2	nfal	⊢ Ⅎ 𝑦 ∀ 𝑥 Ⅎ 𝑦 𝜑
4		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 Ⅎ 𝑦 𝜑
5		sp	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → Ⅎ 𝑦 𝜑 )
6		nfvd	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → Ⅎ 𝑦 𝑥 = 𝑢 )
7	5 6	nfimd	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → Ⅎ 𝑦 ( 𝜑 → 𝑥 = 𝑢 ) )
8	4 7	nfald	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → Ⅎ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑢 ) )
9		equequ2	⊢ ( 𝑢 = 𝑦 → ( 𝑥 = 𝑢 ↔ 𝑥 = 𝑦 ) )
10	9	imbi2d	⊢ ( 𝑢 = 𝑦 → ( ( 𝜑 → 𝑥 = 𝑢 ) ↔ ( 𝜑 → 𝑥 = 𝑦 ) ) )
11	10	albidv	⊢ ( 𝑢 = 𝑦 → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑢 ) ↔ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) )
12	11	a1i	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( 𝑢 = 𝑦 → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑢 ) ↔ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) ) )
13	3 8 12	cbvexdw	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃ 𝑢 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑢 ) ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) )
14	1 13	bitrid	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) )