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 ⊢ ∀ x ∈ z ∃! y φ → ∃ w ∀ x ∈ z ∃ y ∈ w φ

Proof

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