Metamath Proof Explorer

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 
|- ( 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ f M |=. Ax-Rep*
2 nfv 
 |-  F/ w M |=. Ax-Rep*
3 nfv 
 |-  F/ x M |=. Ax-Rep*
4 nfv 
 |-  F/ y M |=. Ax-Rep*
5 nfv 
 |-  F/ z M |=. Ax-Rep*
6 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 ) ) ) ) )
7 6 biimpi 
 |-  ( 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 ) ) ) ) )
8 7 19.21bi 
 |-  ( 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 ) ) ) ) )
9 1 2 3 4 5 8 srepdf 
 |-  ( 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 ) ) ) )