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

Metamath Proof Explorer

Theorem axrep4

Description: A more traditional version of the Axiom of Replacement. (Contributed by NM, 14-Aug-1994) (Proof shortened by Matthew House, 18-Sep-2025)

Ref Expression
Hypothesis axrep4.1 ⊢ Ⅎ z φ
Assertion axrep4 ⊢ ∀ x ∃ z ∀ y φ → y = z → ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ φ

Proof

Step Hyp Ref Expression
1 axrep4.1 ⊢ Ⅎ z φ
2 ax-rep ⊢ ∀ x ∃ z ∀ y ∀ z φ → y = z → ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ ∀ z φ
3 1 19.3 ⊢ ∀ z φ ↔ φ
4 3 imbi1i ⊢ ∀ z φ → y = z ↔ φ → y = z
5 4 albii ⊢ ∀ y ∀ z φ → y = z ↔ ∀ y φ → y = z
6 5 exbii ⊢ ∃ z ∀ y ∀ z φ → y = z ↔ ∃ z ∀ y φ → y = z
7 6 albii ⊢ ∀ x ∃ z ∀ y ∀ z φ → y = z ↔ ∀ x ∃ z ∀ y φ → y = z
8 3 anbi2i ⊢ x ∈ w ∧ ∀ z φ ↔ x ∈ w ∧ φ
9 8 exbii ⊢ ∃ x x ∈ w ∧ ∀ z φ ↔ ∃ x x ∈ w ∧ φ
10 9 bibi2i ⊢ y ∈ z ↔ ∃ x x ∈ w ∧ ∀ z φ ↔ y ∈ z ↔ ∃ x x ∈ w ∧ φ
11 10 albii ⊢ ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ ∀ z φ ↔ ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ φ
12 11 exbii ⊢ ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ ∀ z φ ↔ ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ φ
13 2 7 12 3imtr3i ⊢ ∀ x ∃ z ∀ y φ → y = z → ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ φ