Metamath Proof Explorer

Theorem axrep2

Description: Axiom of Replacement expressed with the fewest number of different variables and without any restrictions on ph . (Contributed by NM, 15-Aug-2003) Remove dependency on ax-13 . (Revised by BJ, 31-May-2019)

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

Proof

Step Hyp Ref Expression
1 nfe1 ⊢ Ⅎ w ∃ w ∀ z ∀ y φ → z = w
2 nfv ⊢ Ⅎ w ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ
3 1 2 nfim ⊢ Ⅎ w ∃ w ∀ z ∀ y φ → z = w → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ
4 3 nfex ⊢ Ⅎ w ∃ x ∃ w ∀ z ∀ y φ → z = w → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ
5 axreplem ⊢ w = y → ∃ x ∃ w ∀ z ∀ y φ → z = w → ∀ z z ∈ x ↔ ∃ x x ∈ w ∧ ∀ y φ ↔ ∃ x ∃ w ∀ z ∀ y φ → z = w → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ
6 axrep1 ⊢ ∃ x ∃ w ∀ z ∀ y φ → z = w → ∀ z z ∈ x ↔ ∃ x x ∈ w ∧ ∀ y φ
7 4 5 6 chvarfv ⊢ ∃ x ∃ w ∀ z ∀ y φ → z = w → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ
8 sp ⊢ ∀ y φ → φ
9 8 imim1i ⊢ φ → z = y → ∀ y φ → z = y
10 9 alimi ⊢ ∀ z φ → z = y → ∀ z ∀ y φ → z = y
11 10 eximi ⊢ ∃ y ∀ z φ → z = y → ∃ y ∀ z ∀ y φ → z = y
12 nfv ⊢ Ⅎ w ∀ z ∀ y φ → z = y
13 nfa1 ⊢ Ⅎ y ∀ y φ
14 nfv ⊢ Ⅎ y z = w
15 13 14 nfim ⊢ Ⅎ y ∀ y φ → z = w
16 15 nfal ⊢ Ⅎ y ∀ z ∀ y φ → z = w
17 equequ2 ⊢ y = w → z = y ↔ z = w
18 17 imbi2d ⊢ y = w → ∀ y φ → z = y ↔ ∀ y φ → z = w
19 18 albidv ⊢ y = w → ∀ z ∀ y φ → z = y ↔ ∀ z ∀ y φ → z = w
20 12 16 19 cbvexv1 ⊢ ∃ y ∀ z ∀ y φ → z = y ↔ ∃ w ∀ z ∀ y φ → z = w
21 11 20 sylib ⊢ ∃ y ∀ z φ → z = y → ∃ w ∀ z ∀ y φ → z = w
22 21 imim1i ⊢ ∃ w ∀ z ∀ y φ → z = w → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ → ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ
23 7 22 eximii ⊢ ∃ x ∃ y ∀ z φ → z = y → ∀ z z ∈ x ↔ ∃ x x ∈ y ∧ ∀ y φ