Theorem vsmrep

Description: The universe is a standard model of the strong Axiom Scheme of Replacement. (Contributed by BTernaryTau, 2-Oct-2026)

	Ref	Expression
Assertion	vsmrep	|- _V |=. Ax-Rep*

Proof

Step	Hyp	Ref	Expression
1		df-smrep	|- ( _V |=. Ax-Rep* <-> A. f A. x e. _V ( A. w e. _V E. y e. _V A. z e. _V ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) -> E. y e. _V A. z e. _V ( z e. y <-> E. w e. _V ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) ) )
2		ax-rep	|- ( A. w E. y A. z ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) -> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) )
3		ralv	|- ( A. w e. _V E. y e. _V A. z e. _V ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) <-> A. w E. y e. _V A. z e. _V ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) )
4		rexv	|- ( E. y e. _V A. z e. _V ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) <-> E. y A. z e. _V ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) )
5		ralv	|- ( A. z e. _V ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) <-> A. z ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) )
6	5	exbii	|- ( E. y A. z e. _V ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) <-> E. y A. z ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) )
7	4 6	bitri	|- ( E. y e. _V A. z e. _V ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) <-> E. y A. z ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) )
8	7	albii	|- ( A. w E. y e. _V A. z e. _V ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) <-> A. w E. y A. z ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) )
9	3 8	bitri	|- ( A. w e. _V E. y e. _V A. z e. _V ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) <-> A. w E. y A. z ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) )
10		rexv	|- ( E. y e. _V A. z e. _V ( z e. y <-> E. w e. _V ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) <-> E. y A. z e. _V ( z e. y <-> E. w e. _V ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) )
11		ralv	|- ( A. z e. _V ( z e. y <-> E. w e. _V ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) <-> A. z ( z e. y <-> E. w e. _V ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) )
12		rexv	|- ( E. w e. _V ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) <-> E. w ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) )
13	12	bibi2i	|- ( ( z e. y <-> E. w e. _V ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) <-> ( z e. y <-> E. w ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) )
14	13	albii	|- ( A. z ( z e. y <-> E. w e. _V ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) <-> A. z ( z e. y <-> E. w ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) )
15	11 14	bitri	|- ( A. z e. _V ( z e. y <-> E. w e. _V ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) <-> A. z ( z e. y <-> E. w ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) )
16	15	exbii	|- ( E. y A. z e. _V ( z e. y <-> E. w e. _V ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) <-> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) )
17	10 16	bitri	|- ( E. y e. _V A. z e. _V ( z e. y <-> E. w e. _V ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) <-> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) )
18	2 9 17	3imtr4i	|- ( A. w e. _V E. y e. _V A. z e. _V ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) -> E. y e. _V A. z e. _V ( z e. y <-> E. w e. _V ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) )
19	18	rgenw	|- A. x e. _V ( A. w e. _V E. y e. _V A. z e. _V ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) -> E. y e. _V A. z e. _V ( z e. y <-> E. w e. _V ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) )
20	1 19	mpgbir	|- _V |=. Ax-Rep*