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) Shorten proof and reduce axiom dependencies. (Revised by BJ, 5-Apr-2026)

	Ref	Expression
Assertion	zfrep6	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		euex	⊢ ( ∃! 𝑦 𝜑 → ∃ 𝑦 𝜑 )
2	1	ralimi	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 𝜑 )
3		df-ral	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ∃! 𝑦 𝜑 ) )
4		eumo	⊢ ( ∃! 𝑦 𝜑 → ∃* 𝑦 𝜑 )
5	4	imim2i	⊢ ( ( 𝑥 ∈ 𝑧 → ∃! 𝑦 𝜑 ) → ( 𝑥 ∈ 𝑧 → ∃* 𝑦 𝜑 ) )
6		moanimv	⊢ ( ∃* 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝑧 → ∃* 𝑦 𝜑 ) )
7	5 6	sylibr	⊢ ( ( 𝑥 ∈ 𝑧 → ∃! 𝑦 𝜑 ) → ∃* 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
8	7	alimi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → ∃! 𝑦 𝜑 ) → ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
9	3 8	sylbi	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
10		axrep6	⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) → ∃ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )
11		rexanid	⊢ ( ∃ 𝑥 ∈ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ↔ ∃ 𝑥 ∈ 𝑧 𝜑 )
12	11	bibi2i	⊢ ( ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ↔ ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜑 ) )
13	12	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜑 ) )
14	13	exbii	⊢ ( ∃ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ↔ ∃ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜑 ) )
15	10 14	sylib	⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) → ∃ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜑 ) )
16	9 15	syl	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ∃ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜑 ) )
17		replem	⊢ ( ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 𝜑 ∧ ∃ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜑 ) ) → ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 )
18	2 16 17	syl2anc	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃! 𝑦 𝜑 → ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 )