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	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		19.42v	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝑧 ∧ ∃ 𝑦 𝜑 ) )
2	1	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝑧 ∧ ∃ 𝑦 𝜑 ) }
3		dmopab	⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) }
4		df-rab	⊢ { 𝑥 ∈ 𝑧 ∣ ∃ 𝑦 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝑧 ∧ ∃ 𝑦 𝜑 ) }
5	2 3 4	3eqtr4i	⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } = { 𝑥 ∈ 𝑧 ∣ ∃ 𝑦 𝜑 }
6		euex	⊢ ( ∃! 𝑦 𝜑 → ∃ 𝑦 𝜑 )
7	6	ralimi	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 𝜑 )
8		rabid2	⊢ ( 𝑧 = { 𝑥 ∈ 𝑧 ∣ ∃ 𝑦 𝜑 } ↔ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 𝜑 )
9	7 8	sylibr	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → 𝑧 = { 𝑥 ∈ 𝑧 ∣ ∃ 𝑦 𝜑 } )
10	5 9	eqtr4id	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } = 𝑧 )
11		vex	⊢ 𝑧 ∈ V
12	10 11	eqeltrdi	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ∈ V )
13		eumo	⊢ ( ∃! 𝑦 𝜑 → ∃* 𝑦 𝜑 )
14	13	imim2i	⊢ ( ( 𝑥 ∈ 𝑧 → ∃! 𝑦 𝜑 ) → ( 𝑥 ∈ 𝑧 → ∃* 𝑦 𝜑 ) )
15		moanimv	⊢ ( ∃* 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝑧 → ∃* 𝑦 𝜑 ) )
16	14 15	sylibr	⊢ ( ( 𝑥 ∈ 𝑧 → ∃! 𝑦 𝜑 ) → ∃* 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
17	16	alimi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ∃! 𝑦 𝜑 ) → ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
18		df-ral	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ∃! 𝑦 𝜑 ) )
19		funopab	⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
20	17 18 19	3imtr4i	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } )
21		funrnex	⊢ ( dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ∈ V → ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } → ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ∈ V ) )
22	12 20 21	sylc	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ∈ V )
23		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑
24	10	eleq2d	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ( 𝑥 ∈ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ↔ 𝑥 ∈ 𝑧 ) )
25		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
26		vex	⊢ 𝑥 ∈ V
27		vex	⊢ 𝑦 ∈ V
28	26 27	opelrn	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } → 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } )
29	25 28	sylbir	⊢ ( ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) → 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } )
30	29	ex	⊢ ( 𝑥 ∈ 𝑧 → ( 𝜑 → 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ) )
31	30	impac	⊢ ( ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) → ( 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ∧ 𝜑 ) )
32	31	eximi	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) → ∃ 𝑦 ( 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ∧ 𝜑 ) )
33	3	abeq2i	⊢ ( 𝑥 ∈ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
34		df-rex	⊢ ( ∃ 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } 𝜑 ↔ ∃ 𝑦 ( 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } ∧ 𝜑 ) )
35	32 33 34	3imtr4i	⊢ ( 𝑥 ∈ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } → ∃ 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } 𝜑 )
36	24 35	syl6bir	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ( 𝑥 ∈ 𝑧 → ∃ 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } 𝜑 ) )
37	23 36	ralrimi	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } 𝜑 )
38		nfopab1	⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) }
39	38	nfrn	⊢ Ⅎ 𝑥 ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) }
40	39	nfeq2	⊢ Ⅎ 𝑥 𝑤 = ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) }
41		nfcv	⊢ Ⅎ 𝑦 𝑤
42		nfopab2	⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) }
43	42	nfrn	⊢ Ⅎ 𝑦 ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) }
44	41 43	rexeqf	⊢ ( 𝑤 = ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } → ( ∃ 𝑦 ∈ 𝑤 𝜑 ↔ ∃ 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } 𝜑 ) )
45	40 44	ralbid	⊢ ( 𝑤 = ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } → ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 ↔ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) } 𝜑 ) )
46	22 37 45	spcedv	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 )