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	Could not format assertion : No typesetting found for |- ( M |=. Ax-Rep* -> A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ph -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ph ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nfv	Could not format F/ f M |=. Ax-Rep* : No typesetting found for |- F/ f M |=. Ax-Rep* with typecode |-
2		nfv	Could not format F/ w M |=. Ax-Rep* : No typesetting found for |- F/ w M |=. Ax-Rep* with typecode |-
3		nfv	Could not format F/ x M |=. Ax-Rep* : No typesetting found for |- F/ x M |=. Ax-Rep* with typecode |-
4		nfv	Could not format F/ y M |=. Ax-Rep* : No typesetting found for |- F/ y M |=. Ax-Rep* with typecode |-
5		nfv	Could not format F/ z M |=. Ax-Rep* : No typesetting found for |- F/ z M |=. Ax-Rep* with typecode |-
6		df-smrep	Could not format ( M |=. Ax-Rep* <-> A. f A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) ) ) : No typesetting found for |- ( M |=. Ax-Rep* <-> A. f A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) ) ) with typecode |-
7	6	biimpi	Could not format ( M |=. Ax-Rep* -> A. f A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) ) ) : No typesetting found for |- ( M |=. Ax-Rep* -> A. f A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) ) ) with typecode |-
8	7	19.21bi	Could not format ( M |=. Ax-Rep* -> A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) ) ) : No typesetting found for |- ( M |=. Ax-Rep* -> A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) ) ) with typecode |-
9	1 2 3 4 5 8	srepdf	Could not format ( M |=. Ax-Rep* -> A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ph -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ph ) ) ) ) : No typesetting found for |- ( M |=. Ax-Rep* -> A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ph -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ph ) ) ) ) with typecode |-