This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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