Theorem zfrep6 6771

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 4543 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 4533. (Contributed by NM, 10-Oct-2003.)

Assertion

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

Distinct variable groups:   ph, w   x, y, z, w

Allowed substitution hints:   ph( x, y, z)

Proof of Theorem zfrep6

Step	Hyp	Ref	Expression
1		euex 2290	. . . . . . 7 |- ( E! y ph -> E. y ph )
2	1	ralimi 2818	. . . . . 6 |- ( A. x e. z E! y ph -> A. x e. z E. y ph )
3		rabid2 3006	. . . . . 6 |- ( z = { x e. z | E. y ph } <-> A. x e. z E. y ph )
4	2, 3	sylibr 215	. . . . 5 |- ( A. x e. z E! y ph -> z = { x e. z | E. y ph } )
5		19.42v 1823	. . . . . . 7 |- ( E. y ( x e. z /\ ph ) <-> ( x e. z /\ E. y ph ) )
6	5	abbii 2556	. . . . . 6 |- { x | E. y ( x e. z /\ ph ) } = { x | ( x e. z /\ E. y ph ) }
7		dmopab 5060	. . . . . 6 |- dom { <. x , y >. | ( x e. z /\ ph ) } = { x | E. y ( x e. z /\ ph ) }
8		df-rab 2784	. . . . . 6 |- { x e. z | E. y ph } = { x | ( x e. z /\ E. y ph ) }
9	6, 7, 8	3eqtr4i 2461	. . . . 5 |- dom { <. x , y >. | ( x e. z /\ ph ) } = { x e. z | E. y ph }
10	4, 9	syl6reqr 2482	. . . 4 |- ( A. x e. z E! y ph -> dom { <. x , y >. | ( x e. z /\ ph ) } = z )
11		vex 3084	. . . 4 |- z e. _V
12	10, 11	syl6eqel 2518	. . 3 |- ( A. x e. z E! y ph -> dom { <. x , y >. | ( x e. z /\ ph ) } e. _V )
13		eumo 2295	. . . . . . 7 |- ( E! y ph -> E* y ph )
14	13	imim2i 16	. . . . . 6 |- ( ( x e. z -> E! y ph ) -> ( x e. z -> E* y ph ) )
15		moanimv 2327	. . . . . 6 |- ( E* y ( x e. z /\ ph ) <-> ( x e. z -> E* y ph ) )
16	14, 15	sylibr 215	. . . . 5 |- ( ( x e. z -> E! y ph ) -> E* y ( x e. z /\ ph ) )
17	16	alimi 1680	. . . 4 |- ( A. x ( x e. z -> E! y ph ) -> A. x E* y ( x e. z /\ ph ) )
18		df-ral 2780	. . . 4 |- ( A. x e. z E! y ph <-> A. x ( x e. z -> E! y ph ) )
19		funopab 5630	. . . 4 |- ( Fun { <. x , y >. | ( x e. z /\ ph ) } <-> A. x E* y ( x e. z /\ ph ) )
20	17, 18, 19	3imtr4i 269	. . 3 |- ( A. x e. z E! y ph -> Fun { <. x , y >. | ( x e. z /\ ph ) } )
21		funrnex 6770	. . 3 |- ( 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 62	. 2 |- ( A. x e. z E! y ph -> ran { <. x , y >. | ( x e. z /\ ph ) } e. _V )
23		nfra1 2806	. . 3 |- F/ x A. x e. z E! y ph
24	10	eleq2d 2492	. . . 4 |- ( A. x e. z E! y ph -> ( x e. dom { <. x , y >. | ( x e. z /\ ph ) } <-> x e. z ) )
25		opabid 4723	. . . . . . . . 9 |- ( <. x , y >. e. { <. x , y >. | ( x e. z /\ ph ) } <-> ( x e. z /\ ph ) )
26		vex 3084	. . . . . . . . . 10 |- x e. _V
27		vex 3084	. . . . . . . . . 10 |- y e. _V
28	26, 27	opelrn 5081	. . . . . . . . 9 |- ( <. x , y >. e. { <. x , y >. | ( x e. z /\ ph ) } -> y e. ran { <. x , y >. | ( x e. z /\ ph ) } )
29	25, 28	sylbir 216	. . . . . . . 8 |- ( ( x e. z /\ ph ) -> y e. ran { <. x , y >. | ( x e. z /\ ph ) } )
30	29	ex 435	. . . . . . 7 |- ( x e. z -> ( ph -> y e. ran { <. x , y >. | ( x e. z /\ ph ) } ) )
31	30	impac 625	. . . . . 6 |- ( ( x e. z /\ ph ) -> ( y e. ran { <. x , y >. | ( x e. z /\ ph ) } /\ ph ) )
32	31	eximi 1702	. . . . 5 |- ( E. y ( x e. z /\ ph ) -> E. y ( y e. ran { <. x , y >. | ( x e. z /\ ph ) } /\ ph ) )
33	7	abeq2i 2549	. . . . 5 |- ( x e. dom { <. x , y >. | ( x e. z /\ ph ) } <-> E. y ( x e. z /\ ph ) )
34		df-rex 2781	. . . . 5 |- ( 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 269	. . . 4 |- ( x e. dom { <. x , y >. | ( x e. z /\ ph ) } -> E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph )
36	24, 35	syl6bir 232	. . 3 |- ( 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 2825	. 2 |- ( A. x e. z E! y ph -> A. x e. z E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph )
38		nfopab1 4487	. . . . . 6 |- F/_ x { <. x , y >. | ( x e. z /\ ph ) }
39	38	nfrn 5092	. . . . 5 |- F/_ x ran { <. x , y >. | ( x e. z /\ ph ) }
40	39	nfeq2 2601	. . . 4 |- F/ x w = ran { <. x , y >. | ( x e. z /\ ph ) }
41		nfcv 2584	. . . . 5 |- F/_ y w
42		nfopab2 4488	. . . . . 6 |- F/_ y { <. x , y >. | ( x e. z /\ ph ) }
43	42	nfrn 5092	. . . . 5 |- F/_ y ran { <. x , y >. | ( x e. z /\ ph ) }
44	41, 43	rexeqf 3022	. . . 4 |- ( 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 2859	. . 3 |- ( 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	45	spcegv 3167	. 2 |- ( ran { <. x , y >. | ( x e. z /\ ph ) } e. _V -> ( A. x e. z E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph -> E. w A. x e. z E. y e. w ph ) )
47	22, 37, 46	sylc 62	1 |- ( A. x e. z E! y ph -> E. w A. x e. z E. y e. w ph )

Syntax hints:   -> wi 4   /\ wa 370   A.wal 1435   = wceq 1437   E.wex 1659   e. wcel 1868   E!weu 2265   E*wmo 2266   {cab 2407   A.wral 2775   E.wrex 2776   {crab 2779   _Vcvv 3081   <.cop 4002   {copab 4478   dom cdm 4849   ran crn 4850   Fun wfun 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pr 4656  ax-un 6593

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605

This theorem is referenced by:  bnj865  29729