Metamath Proof Explorer

Theorem axrep4

Description: A more traditional version of the Axiom of Replacement. (Contributed by NM, 14-Aug-1994)

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 axrep3 ⊢ ∃ x ∃ z ∀ y φ → y = z → ∀ y y ∈ x ↔ ∃ x x ∈ w ∧ ∀ z φ
3 2 19.35i ⊢ ∀ x ∃ z ∀ y φ → y = z → ∃ x ∀ y y ∈ x ↔ ∃ x x ∈ w ∧ ∀ z φ
4 nfv ⊢ Ⅎ z y ∈ x
5 nfv ⊢ Ⅎ z x ∈ w
6 nfa1 ⊢ Ⅎ z ∀ z φ
7 5 6 nfan ⊢ Ⅎ z x ∈ w ∧ ∀ z φ
8 7 nfex ⊢ Ⅎ z ∃ x x ∈ w ∧ ∀ z φ
9 4 8 nfbi ⊢ Ⅎ z y ∈ x ↔ ∃ x x ∈ w ∧ ∀ z φ
10 9 nfal ⊢ Ⅎ z ∀ y y ∈ x ↔ ∃ x x ∈ w ∧ ∀ z φ
11 nfv ⊢ Ⅎ x y ∈ z
12 nfe1 ⊢ Ⅎ x ∃ x x ∈ w ∧ φ
13 11 12 nfbi ⊢ Ⅎ x y ∈ z ↔ ∃ x x ∈ w ∧ φ
14 13 nfal ⊢ Ⅎ x ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ φ
15 elequ2 ⊢ x = z → y ∈ x ↔ y ∈ z
16 1 19.3 ⊢ ∀ z φ ↔ φ
17 16 anbi2i ⊢ x ∈ w ∧ ∀ z φ ↔ x ∈ w ∧ φ
18 17 exbii ⊢ ∃ x x ∈ w ∧ ∀ z φ ↔ ∃ x x ∈ w ∧ φ
19 18 a1i ⊢ x = z → ∃ x x ∈ w ∧ ∀ z φ ↔ ∃ x x ∈ w ∧ φ
20 15 19 bibi12d ⊢ x = z → y ∈ x ↔ ∃ x x ∈ w ∧ ∀ z φ ↔ y ∈ z ↔ ∃ x x ∈ w ∧ φ
21 20 albidv ⊢ x = z → ∀ y y ∈ x ↔ ∃ x x ∈ w ∧ ∀ z φ ↔ ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ φ
22 10 14 21 cbvexv1 ⊢ ∃ x ∀ y y ∈ x ↔ ∃ x x ∈ w ∧ ∀ z φ ↔ ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ φ
23 3 22 sylib ⊢ ∀ x ∃ z ∀ y φ → y = z → ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ φ