Metamath Proof Explorer

Theorem axrep3

Description: Axiom of Replacement slightly strengthened from axrep2 ; w may occur free in ph . (Contributed by NM, 2-Jan-1997) Remove dependency on ax-13 . (Revised by BJ, 31-May-2019)

Ref Expression
Assertion axrep3 ⊢ ∃ x ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ w ∧ ∀ y φ

Proof

Step Hyp Ref Expression
1 nfe1 ⊢ Ⅎ y ∃ y ∀ z φ → z = y
2 nfv ⊢ Ⅎ y z ∈ x
3 nfv ⊢ Ⅎ y x ∈ w
4 nfa1 ⊢ Ⅎ y ∀ y φ
5 3 4 nfan ⊢ Ⅎ y x ∈ w ∧ ∀ y φ
6 5 nfex ⊢ Ⅎ y ∃ x x ∈ w ∧ ∀ y φ
7 2 6 nfbi ⊢ Ⅎ y z ∈ x ↔ ∃ x x ∈ w ∧ ∀ y φ
8 7 nfal ⊢ Ⅎ y ∀ z z ∈ x ↔ ∃ x x ∈ w ∧ ∀ y φ
9 1 8 nfim ⊢ Ⅎ y ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ w ∧ ∀ y φ
10 9 nfex ⊢ Ⅎ y ∃ x ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ w ∧ ∀ y φ
11 axreplem ⊢ y = w → ∃ x ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ ↔ ∃ x ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ w ∧ ∀ y φ
12 axrep2 ⊢ ∃ x ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ
13 10 11 12 chvarfv ⊢ ∃ x ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ w ∧ ∀ y φ