Theorem smrepsrep

Description: Derive the strong version of the Axiom Scheme of Replacement used in wfaxrep (see comments there) from M |=. Ax-Rep* . (Contributed by BTernaryTau, 30-Sep-2026)

	Ref	Expression
Assertion	smrepsrep	⊢ ( 𝑀 ⊨ Ax-Rep* → ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑓 𝑀 ⊨ Ax-Rep*
2		nfv	⊢ Ⅎ 𝑤 𝑀 ⊨ Ax-Rep*
3		nfv	⊢ Ⅎ 𝑥 𝑀 ⊨ Ax-Rep*
4		nfv	⊢ Ⅎ 𝑦 𝑀 ⊨ Ax-Rep*
5		nfv	⊢ Ⅎ 𝑧 𝑀 ⊨ Ax-Rep*
6		df-smrep	⊢ ( 𝑀 ⊨ Ax-Rep* ↔ ∀ 𝑓 ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
7	6	biimpi	⊢ ( 𝑀 ⊨ Ax-Rep* → ∀ 𝑓 ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
8	7	19.21bi	⊢ ( 𝑀 ⊨ Ax-Rep* → ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
9	1 2 3 4 5 8	srepdf	⊢ ( 𝑀 ⊨ Ax-Rep* → ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )