Metamath Proof Explorer


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 x z ∃! y φ w x z y w φ

Proof

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