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	$⊢ \forall x \in z \exists! y φ \to \exists w \forall x \in z \exists y \in w φ$

Proof

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

Metamath Proof Explorer

Theorem zfrep6

Proof