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→∀zz∈x↔∃xx∈y∧∀yφ

Proof

Step Hyp Ref Expression
1 nfe1 ⊢Ⅎw∃w∀z∀yφ→z=w
2 nfv ⊢Ⅎw∀zz∈x↔∃xx∈y∧∀yφ
3 1 2 nfim ⊢Ⅎw∃w∀z∀yφ→z=w→∀zz∈x↔∃xx∈y∧∀yφ
4 3 nfex ⊢Ⅎw∃x∃w∀z∀yφ→z=w→∀zz∈x↔∃xx∈y∧∀yφ
5 axreplem ⊢w=y→∃x∃w∀z∀yφ→z=w→∀zz∈x↔∃xx∈w∧∀yφ↔∃x∃w∀z∀yφ→z=w→∀zz∈x↔∃xx∈y∧∀yφ
6 axrep1 ⊢∃x∃w∀z∀yφ→z=w→∀zz∈x↔∃xx∈w∧∀yφ
7 4 5 6 chvarfv ⊢∃x∃w∀z∀yφ→z=w→∀zz∈x↔∃xx∈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 ⊢Ⅎyz=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→∀zz∈x↔∃xx∈y∧∀yφ→∃y∀zφ→z=y→∀zz∈x↔∃xx∈y∧∀yφ
23 7 22 eximii ⊢∃x∃y∀zφ→z=y→∀zz∈x↔∃xx∈y∧∀yφ