Definition df-smrep

Description: Define the strong Axiom Scheme of Replacement predicate, which is true for a class that is a standard model of the strong version of the Axiom Scheme of Replacement used in wfaxrep (see comments there). Our notation includes an asterisk because we cannot guarantee that a standard model of the Axiom Scheme of Replacement will also be a standard model of this strong version. However, proving that a class is a standard model of the strong Axiom Scheme of Replacement is sufficient to prove that it is also a standard model of the ZF Axiom Scheme of Replacement.

The exact expression used in wfaxrep is unsuitable for use in a definition because it contains a wff metavariable that we cannot quantify over. Instead, this definition uses the specific instance where ph is replaced with ( Fun f /\ w e. dom f /\ ( fw ) = z ) . This allows the set f to effectively take on the role of the function-like wff, and since f is a setvar, we are free to add a universal quantifier over it. The full scheme can then be recovered from this definition using smrepsrep .

This approach works because we can use our ax-rep to guarantee the existence of a suitable f in _V for any x and function-like ph . Note that M is not guaranteed to contain a suitable f (since it might not model the necessary axioms), so we must use an unrestricted universal quantifier for f .

(Contributed by BTernaryTau, 30-Sep-2026)

	Ref	Expression
Assertion	df-smrep	|- ( 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 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cM	|- M
1	0	wsmrep	|- M |=. Ax-Rep*
2		vf	|- f
3		vx	|- x
4		vw	|- w
5		vy	|- y
6		vz	|- z
7	2	cv	|- f
8	7	wfun	|- Fun f
9	4	cv	|- w
10	7	cdm	|- dom f
11	9 10	wcel	|- w e. dom f
12	9 7	cfv	|- ( f ` w )
13	6	cv	|- z
14	12 13	wceq	|- ( f ` w ) = z
15	8 11 14	w3a	|- ( Fun f /\ w e. dom f /\ ( f ` w ) = z )
16	15 5	wal	|- A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z )
17	5	cv	|- y
18	13 17	wceq	|- z = y
19	16 18	wi	|- ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y )
20	19 6 0	wral	|- A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y )
21	20 5 0	wrex	|- E. y e. M A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y )
22	21 4 0	wral	|- 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 )
23	13 17	wcel	|- z e. y
24	3	cv	|- x
25	9 24	wcel	|- w e. x
26	25 16	wa	|- ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) )
27	26 4 0	wrex	|- E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) )
28	23 27	wb	|- ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) )
29	28 6 0	wral	|- 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 ) ) )
30	29 5 0	wrex	|- 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 ) ) )
31	22 30	wi	|- ( 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 ) ) ) )
32	31 3 0	wral	|- 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 ) ) ) )
33	32 2	wal	|- 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 ) ) ) )
34	1 33	wb	|- ( 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 ) ) ) ) )