Theorem zfrep6

Description: A version of the Axiom of Replacement. Normally ph would have free variables x and y . Axiom 6 of Kunen p. 12. The Separation Scheme ax-sep cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version in place of our ax-rep . (Contributed by NM, 10-Oct-2003)

	Ref	Expression
Assertion	zfrep6	|- ( A. x e. z E! y ph -> E. w A. x e. z E. y e. w ph )

Proof

Step	Hyp	Ref	Expression
1		euex	|- ( E! y ph -> E. y ph )
2	1	ralimi	|- ( A. x e. z E! y ph -> A. x e. z E. y ph )
3		rabid2	|- ( z = { x e. z | E. y ph } <-> A. x e. z E. y ph )
4	2 3	sylibr	|- ( A. x e. z E! y ph -> z = { x e. z | E. y ph } )
5		19.42v	|- ( E. y ( x e. z /\ ph ) <-> ( x e. z /\ E. y ph ) )
6	5	abbii	|- { x | E. y ( x e. z /\ ph ) } = { x | ( x e. z /\ E. y ph ) }
7		dmopab	|- dom { <. x , y >. | ( x e. z /\ ph ) } = { x | E. y ( x e. z /\ ph ) }
8		df-rab	|- { x e. z | E. y ph } = { x | ( x e. z /\ E. y ph ) }
9	6 7 8	3eqtr4i	|- dom { <. x , y >. | ( x e. z /\ ph ) } = { x e. z | E. y ph }
10	4 9	syl6reqr	|- ( A. x e. z E! y ph -> dom { <. x , y >. | ( x e. z /\ ph ) } = z )
11		vex	|- z e. _V
12	10 11	eqeltrdi	|- ( A. x e. z E! y ph -> dom { <. x , y >. | ( x e. z /\ ph ) } e. _V )
13		eumo	|- ( E! y ph -> E* y ph )
14	13	imim2i	|- ( ( x e. z -> E! y ph ) -> ( x e. z -> E* y ph ) )
15		moanimv	|- ( E* y ( x e. z /\ ph ) <-> ( x e. z -> E* y ph ) )
16	14 15	sylibr	|- ( ( x e. z -> E! y ph ) -> E* y ( x e. z /\ ph ) )
17	16	alimi	|- ( A. x ( x e. z -> E! y ph ) -> A. x E* y ( x e. z /\ ph ) )
18		df-ral	|- ( A. x e. z E! y ph <-> A. x ( x e. z -> E! y ph ) )
19		funopab	|- ( Fun { <. x , y >. | ( x e. z /\ ph ) } <-> A. x E* y ( x e. z /\ ph ) )
20	17 18 19	3imtr4i	|- ( A. x e. z E! y ph -> Fun { <. x , y >. | ( x e. z /\ ph ) } )
21		funrnex	|- ( dom { <. x , y >. | ( x e. z /\ ph ) } e. _V -> ( Fun { <. x , y >. | ( x e. z /\ ph ) } -> ran { <. x , y >. | ( x e. z /\ ph ) } e. _V ) )
22	12 20 21	sylc	|- ( A. x e. z E! y ph -> ran { <. x , y >. | ( x e. z /\ ph ) } e. _V )
23		nfra1	|- F/ x A. x e. z E! y ph
24	10	eleq2d	|- ( A. x e. z E! y ph -> ( x e. dom { <. x , y >. | ( x e. z /\ ph ) } <-> x e. z ) )
25		opabidw	|- ( <. x , y >. e. { <. x , y >. | ( x e. z /\ ph ) } <-> ( x e. z /\ ph ) )
26		vex	|- x e. _V
27		vex	|- y e. _V
28	26 27	opelrn	|- ( <. x , y >. e. { <. x , y >. | ( x e. z /\ ph ) } -> y e. ran { <. x , y >. | ( x e. z /\ ph ) } )
29	25 28	sylbir	|- ( ( x e. z /\ ph ) -> y e. ran { <. x , y >. | ( x e. z /\ ph ) } )
30	29	ex	|- ( x e. z -> ( ph -> y e. ran { <. x , y >. | ( x e. z /\ ph ) } ) )
31	30	impac	|- ( ( x e. z /\ ph ) -> ( y e. ran { <. x , y >. | ( x e. z /\ ph ) } /\ ph ) )
32	31	eximi	|- ( E. y ( x e. z /\ ph ) -> E. y ( y e. ran { <. x , y >. | ( x e. z /\ ph ) } /\ ph ) )
33	7	abeq2i	|- ( x e. dom { <. x , y >. | ( x e. z /\ ph ) } <-> E. y ( x e. z /\ ph ) )
34		df-rex	|- ( E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph <-> E. y ( y e. ran { <. x , y >. | ( x e. z /\ ph ) } /\ ph ) )
35	32 33 34	3imtr4i	|- ( x e. dom { <. x , y >. | ( x e. z /\ ph ) } -> E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph )
36	24 35	syl6bir	|- ( A. x e. z E! y ph -> ( x e. z -> E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph ) )
37	23 36	ralrimi	|- ( A. x e. z E! y ph -> A. x e. z E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph )
38		nfopab1	|- F/_ x { <. x , y >. | ( x e. z /\ ph ) }
39	38	nfrn	|- F/_ x ran { <. x , y >. | ( x e. z /\ ph ) }
40	39	nfeq2	|- F/ x w = ran { <. x , y >. | ( x e. z /\ ph ) }
41		nfcv	|- F/_ y w
42		nfopab2	|- F/_ y { <. x , y >. | ( x e. z /\ ph ) }
43	42	nfrn	|- F/_ y ran { <. x , y >. | ( x e. z /\ ph ) }
44	41 43	rexeqf	|- ( w = ran { <. x , y >. | ( x e. z /\ ph ) } -> ( E. y e. w ph <-> E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph ) )
45	40 44	ralbid	|- ( w = ran { <. x , y >. | ( x e. z /\ ph ) } -> ( A. x e. z E. y e. w ph <-> A. x e. z E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph ) )
46	22 37 45	spcedv	|- ( A. x e. z E! y ph -> E. w A. x e. z E. y e. w ph )