mof

Description: Version of df-mo with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by NM, 8-Mar-1995) Extract dfmo from this proof, and prove mof from it (as of 30-Sep-2022, directly from df-mo ). (Revised by Wolf Lammen, 28-May-2019) Avoid ax-13 . (Revised by Wolf Lammen, 16-Oct-2022)

		Ref	Expression
	Hypothesis	mof.1	⊢ Ⅎ 𝑦 𝜑
	Assertion	mof	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		mof.1	⊢ Ⅎ 𝑦 𝜑
2		df-mo	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) )
3		nfv	⊢ Ⅎ 𝑦 𝑥 = 𝑧
4	1 3	nfim	⊢ Ⅎ 𝑦 ( 𝜑 → 𝑥 = 𝑧 )
5	4	nfal	⊢ Ⅎ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 )
6		nfv	⊢ Ⅎ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 )
7		equequ2	⊢ ( 𝑧 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑥 = 𝑦 ) )
8	7	imbi2d	⊢ ( 𝑧 = 𝑦 → ( ( 𝜑 → 𝑥 = 𝑧 ) ↔ ( 𝜑 → 𝑥 = 𝑦 ) ) )
9	8	albidv	⊢ ( 𝑧 = 𝑦 → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ↔ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) )
10	5 6 9	cbvexv1	⊢ ( ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
11	2 10	bitri	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )

Metamath Proof Explorer

Theorem mof

Proof