Theorem repizf2 3906

Description: Replacement. This version of replacement is stronger than repizf 3864 in the sense that ph does not need to map all values of x in w to a value of y. The resulting set contains those elements for which there is a value of y and in that sense, this theorem combines repizf 3864 with ax-sep 3866. Another variation would be A.x e. wE*yph -> {y | E.x(x e. w /\ ph) } e. _V but we don't have a proof of that yet. (Contributed by Jim Kingdon, 7-Sep-2018.)

Hypothesis

Ref	Expression
repizf2.1	|- F/zph

Assertion

Ref	Expression
repizf2	|- (A.x e. w E*yph -> E.zA.x e. {x e. w | E.yph }E.y e. z ph)

Distinct variable group:   x,y,z,w

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

Proof of Theorem repizf2

Dummy variable v is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2554	. . 3 |- w e. _V
2	1	rabex 3892	. 2 |- {x e. w | E.yph } e. _V
3		repizf2lem 3905	. . . 4 |- (A.x e. w E*yph <-> A.x e. {x e. w | E.yph }E!yph)
4		nfcv 2175	. . . . . 6 |- F/_xv
5		nfrab1 2483	. . . . . 6 |- F/_x {x e. w | E.yph }
6	4, 5	raleqf 2495	. . . . 5 |- (v = {x e. w | E.yph } -> (A.x e. v E!yph <-> A.x e. {x e. w | E.yph }E!yph))
7		repizf2.1	. . . . . 6 |- F/zph
8	7	repizf 3864	. . . . 5 |- (A.x e. v E!yph -> E.zA.x e. v E.y e. z ph)
9	6, 8	syl6bir 153	. . . 4 |- (v = {x e. w | E.yph } -> (A.x e. {x e. w | E.yph }E!yph -> E.zA.x e. v E.y e. z ph))
10	3, 9	syl5bi 141	. . 3 |- (v = {x e. w | E.yph } -> (A.x e. w E*yph -> E.zA.x e. v E.y e. z ph))
11		df-rab 2309	. . . . . 6 |- {x e. w | E.yph } = {x | (x e. w /\ E.yph) }
12		nfv 1418	. . . . . . . 8 |- F/z x e. w
13	7	nfex 1525	. . . . . . . 8 |- F/zE.yph
14	12, 13	nfan 1454	. . . . . . 7 |- F/z(x e. w /\ E.yph)
15	14	nfab 2179	. . . . . 6 |- F/_z {x | (x e. w /\ E.yph) }
16	11, 15	nfcxfr 2172	. . . . 5 |- F/_z {x e. w | E.yph }
17	16	nfeq2 2186	. . . 4 |- F/z v = {x e. w | E.yph }
18	4, 5	raleqf 2495	. . . 4 |- (v = {x e. w | E.yph } -> (A.x e. v E.y e. z ph <-> A.x e. {x e. w | E.yph }E.y e. z ph))
19	17, 18	exbid 1504	. . 3 |- (v = {x e. w | E.yph } -> (E.zA.x e. v E.y e. z ph <-> E.zA.x e. {x e. w | E.yph }E.y e. z ph))
20	10, 19	sylibd 138	. 2 |- (v = {x e. w | E.yph } -> (A.x e. w E*yph -> E.zA.x e. {x e. w | E.yph }E.y e. z ph))
21	2, 20	vtocle 2621	1 |- (A.x e. w E*yph -> E.zA.x e. {x e. w | E.yph }E.y e. z ph)

Syntax hints:   -> wi 4   /\ wa 97   = wceq 1242   F/wnf 1346  E.wex 1378  E!weu 1897  E*wmo 1898   {cab 2023  A.wral 2300  E.wrex 2301   {crab 2304

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866

This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rab 2309  df-v 2553  df-in 2918  df-ss 2925

This theorem is referenced by: (None)