Metamath Proof Explorer

Theorem srepdf

Description: Derive the strong version of the Axiom Scheme of Replacement used in wfaxrep (see comments there) from a particular instance of that version of Replacement. Note that this theorem depends on ax-rep , so it does not follow that we could replace ax-rep with an axiom that lacks a wff metavariable. (Contributed by BTernaryTau, 30-Sep-2026)

Ref Expression
Hypotheses srepdf.1 
|- F/ f ph
srepdf.2 
|- F/ w ph
srepdf.3 
|- F/ x ph
srepdf.4 
|- F/ y ph
srepdf.5 
|- F/ z ph
srepdf.6 
|- ( ph -> 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 ) ) ) ) )
Assertion srepdf 
|- ( ph -> A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ps ) ) ) )

Proof

Step Hyp Ref Expression
1 srepdf.1 
 |-  F/ f ph
2 srepdf.2 
 |-  F/ w ph
3 srepdf.3 
 |-  F/ x ph
4 srepdf.4 
 |-  F/ y ph
5 srepdf.5 
 |-  F/ z ph
6 srepdf.6 
 |-  ( ph -> 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 ax-5 
 |-  ( A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) -> A. g A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) )
8 nfv 
 |-  F/ g ( ph /\ x e. M )
9 nfa1 
 |-  F/ g A. g A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y )
10 8 9 nfan 
 |-  F/ g ( ( ph /\ x e. M ) /\ A. g A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) )
11 nfv 
 |-  F/ w x e. M
12 2 11 nfan 
 |-  F/ w ( ph /\ x e. M )
13 nfra1 
 |-  F/ w A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y )
14 13 nfal 
 |-  F/ w A. g A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y )
15 12 14 nfan 
 |-  F/ w ( ( ph /\ x e. M ) /\ A. g A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) )
16 nfv 
 |-  F/ y x e. M
17 4 16 nfan 
 |-  F/ y ( ph /\ x e. M )
18 nfcv 
 |-  F/_ y M
19 nfre1 
 |-  F/ y E. y e. M A. z e. M ( A. y ps -> z = y )
20 18 19 nfralw 
 |-  F/ y A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y )
21 20 nfal 
 |-  F/ y A. g A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y )
22 17 21 nfan 
 |-  F/ y ( ( ph /\ x e. M ) /\ A. g A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) )
23 nfv 
 |-  F/ z x e. M
24 5 23 nfan 
 |-  F/ z ( ph /\ x e. M )
25 nfcv 
 |-  F/_ z M
26 nfra1 
 |-  F/ z A. z e. M ( A. y ps -> z = y )
27 25 26 nfrexw 
 |-  F/ z E. y e. M A. z e. M ( A. y ps -> z = y )
28 25 27 nfralw 
 |-  F/ z A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y )
29 28 nfal 
 |-  F/ z A. g A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y )
30 24 29 nfan 
 |-  F/ z ( ( ph /\ x e. M ) /\ A. g A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) )
31 simplr 
 |-  ( ( ( ph /\ x e. M ) /\ A. g A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) ) -> x e. M )
32 1 6 alrimi 
 |-  ( ph -> 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 ) ) ) ) )
33 funeq 
 |-  ( f = g -> ( Fun f <-> Fun g ) )
34 dmeq 
 |-  ( f = g -> dom f = dom g )
35 34 eleq2d 
 |-  ( f = g -> ( w e. dom f <-> w e. dom g ) )
36 fveq1 
 |-  ( f = g -> ( f ` w ) = ( g ` w ) )
37 36 eqeq1d 
 |-  ( f = g -> ( ( f ` w ) = z <-> ( g ` w ) = z ) )
38 33 35 37 3anbi123d 
 |-  ( f = g -> ( ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) <-> ( Fun g /\ w e. dom g /\ ( g ` w ) = z ) ) )
39 38 albidv 
 |-  ( f = g -> ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) <-> A. y ( Fun g /\ w e. dom g /\ ( g ` w ) = z ) ) )
40 39 imbi1d 
 |-  ( f = g -> ( ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) <-> ( A. y ( Fun g /\ w e. dom g /\ ( g ` w ) = z ) -> z = y ) ) )
41 40 rexralbidv 
 |-  ( f = g -> ( 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 ( A. y ( Fun g /\ w e. dom g /\ ( g ` w ) = z ) -> z = y ) ) )
42 41 ralbidv 
 |-  ( f = g -> ( 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 ) <-> A. w e. M E. y e. M A. z e. M ( A. y ( Fun g /\ w e. dom g /\ ( g ` w ) = z ) -> z = y ) ) )
43 39 anbi2d 
 |-  ( f = g -> ( ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) <-> ( w e. x /\ A. y ( Fun g /\ w e. dom g /\ ( g ` w ) = z ) ) ) )
44 43 rexbidv 
 |-  ( f = g -> ( E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) <-> E. w e. M ( w e. x /\ A. y ( Fun g /\ w e. dom g /\ ( g ` w ) = z ) ) ) )
45 44 bibi2d 
 |-  ( f = g -> ( ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) <-> ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun g /\ w e. dom g /\ ( g ` w ) = z ) ) ) ) )
46 45 rexralbidv 
 |-  ( f = g -> ( 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 ) ) ) <-> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun g /\ w e. dom g /\ ( g ` w ) = z ) ) ) ) )
47 42 46 imbi12d 
 |-  ( f = g -> ( ( 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 ) ) ) ) <-> ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun g /\ w e. dom g /\ ( g ` 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 g /\ w e. dom g /\ ( g ` w ) = z ) ) ) ) ) )
48 47 ralbidv 
 |-  ( f = g -> ( 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 ) ) ) ) <-> A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun g /\ w e. dom g /\ ( g ` 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 g /\ w e. dom g /\ ( g ` w ) = z ) ) ) ) ) )
49 48 cbvalvw 
 |-  ( 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 ) ) ) ) <-> A. g A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun g /\ w e. dom g /\ ( g ` 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 g /\ w e. dom g /\ ( g ` w ) = z ) ) ) ) )
50 32 49 sylib 
 |-  ( ph -> A. g A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun g /\ w e. dom g /\ ( g ` 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 g /\ w e. dom g /\ ( g ` w ) = z ) ) ) ) )
51 50 19.21bi 
 |-  ( ph -> A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun g /\ w e. dom g /\ ( g ` 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 g /\ w e. dom g /\ ( g ` w ) = z ) ) ) ) )
52 51 r19.21bi 
 |-  ( ( ph /\ x e. M ) -> ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun g /\ w e. dom g /\ ( g ` 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 g /\ w e. dom g /\ ( g ` w ) = z ) ) ) ) )
53 52 adantr 
 |-  ( ( ( ph /\ x e. M ) /\ A. g A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) ) -> ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun g /\ w e. dom g /\ ( g ` 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 g /\ w e. dom g /\ ( g ` w ) = z ) ) ) ) )
54 simpr 
 |-  ( ( ( ph /\ x e. M ) /\ A. g A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) ) -> A. g A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) )
55 54 19.21bi 
 |-  ( ( ( ph /\ x e. M ) /\ A. g A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) ) -> A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) )
56 eqid 
 |-  ( { <. w , z >. | ( w e. M /\ z e. M /\ A. y ps ) } |` x ) = ( { <. w , z >. | ( w e. M /\ z e. M /\ A. y ps ) } |` x )
57 eqid 
 |-  { <. w , z >. | ( w e. M /\ z e. M /\ A. y ps ) } = { <. w , z >. | ( w e. M /\ z e. M /\ A. y ps ) }
58 10 15 22 30 31 53 55 56 57 srepdflem2 
 |-  ( ( ( ph /\ x e. M ) /\ A. g A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ps ) ) )
59 58 ex 
 |-  ( ( ph /\ x e. M ) -> ( A. g A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ps ) ) ) )
60 7 59 syl5 
 |-  ( ( ph /\ x e. M ) -> ( A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ps ) ) ) )
61 3 60 ralrimia 
 |-  ( ph -> A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ps -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ps ) ) ) )