Metamath Proof Explorer

Theorem zfcndrep

Description: Axiom of Replacement ax-rep , reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 15-Aug-2003) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nfe1 ⊢Ⅎy∃y∀z∀yφ→z=y
2 nfv ⊢Ⅎyz∈w
3 nfv ⊢Ⅎyw∈x
4 nfa1 ⊢Ⅎy∀y∀yφ
5 3 4 nfan ⊢Ⅎyw∈x∧∀y∀yφ
6 5 nfex ⊢Ⅎy∃ww∈x∧∀y∀yφ
7 2 6 nfbi ⊢Ⅎyz∈w↔∃ww∈x∧∀y∀yφ
8 7 nfal ⊢Ⅎy∀zz∈w↔∃ww∈x∧∀y∀yφ
9 1 8 nfim ⊢Ⅎy∃y∀z∀yφ→z=y→∀zz∈w↔∃ww∈x∧∀y∀yφ
10 9 nfex ⊢Ⅎy∃w∃y∀z∀yφ→z=y→∀zz∈w↔∃ww∈x∧∀y∀yφ
11 elequ2 ⊢y=x→w∈y↔w∈x
12 11 anbi1d ⊢y=x→w∈y∧∀y∀yφ↔w∈x∧∀y∀yφ
13 12 exbidv ⊢y=x→∃ww∈y∧∀y∀yφ↔∃ww∈x∧∀y∀yφ
14 13 bibi2d ⊢y=x→z∈w↔∃ww∈y∧∀y∀yφ↔z∈w↔∃ww∈x∧∀y∀yφ
15 14 albidv ⊢y=x→∀zz∈w↔∃ww∈y∧∀y∀yφ↔∀zz∈w↔∃ww∈x∧∀y∀yφ
16 15 imbi2d ⊢y=x→∃y∀z∀yφ→z=y→∀zz∈w↔∃ww∈y∧∀y∀yφ↔∃y∀z∀yφ→z=y→∀zz∈w↔∃ww∈x∧∀y∀yφ
17 16 exbidv ⊢y=x→∃w∃y∀z∀yφ→z=y→∀zz∈w↔∃ww∈y∧∀y∀yφ↔∃w∃y∀z∀yφ→z=y→∀zz∈w↔∃ww∈x∧∀y∀yφ
18 axrepnd ⊢∃w∃y∀z∀yφ→z=y→∀z∀yz∈w↔∃w∀zw∈y∧∀y∀yφ
19 19.3v ⊢∀yz∈w↔z∈w
20 19.3v ⊢∀zw∈y↔w∈y
21 20 anbi1i ⊢∀zw∈y∧∀y∀yφ↔w∈y∧∀y∀yφ
22 21 exbii ⊢∃w∀zw∈y∧∀y∀yφ↔∃ww∈y∧∀y∀yφ
23 19 22 bibi12i ⊢∀yz∈w↔∃w∀zw∈y∧∀y∀yφ↔z∈w↔∃ww∈y∧∀y∀yφ
24 23 albii ⊢∀z∀yz∈w↔∃w∀zw∈y∧∀y∀yφ↔∀zz∈w↔∃ww∈y∧∀y∀yφ
25 24 imbi2i ⊢∃y∀z∀yφ→z=y→∀z∀yz∈w↔∃w∀zw∈y∧∀y∀yφ↔∃y∀z∀yφ→z=y→∀zz∈w↔∃ww∈y∧∀y∀yφ
26 25 exbii ⊢∃w∃y∀z∀yφ→z=y→∀z∀yz∈w↔∃w∀zw∈y∧∀y∀yφ↔∃w∃y∀z∀yφ→z=y→∀zz∈w↔∃ww∈y∧∀y∀yφ
27 18 26 mpbi ⊢∃w∃y∀z∀yφ→z=y→∀zz∈w↔∃ww∈y∧∀y∀yφ
28 10 17 27 chvar ⊢∃w∃y∀z∀yφ→z=y→∀zz∈w↔∃ww∈x∧∀y∀yφ
29 28 19.35i ⊢∀w∃y∀z∀yφ→z=y→∃w∀zz∈w↔∃ww∈x∧∀y∀yφ
30 nfv ⊢Ⅎwz∈y
31 nfe1 ⊢Ⅎw∃ww∈x∧∀yφ
32 30 31 nfbi ⊢Ⅎwz∈y↔∃ww∈x∧∀yφ
33 32 nfal ⊢Ⅎw∀zz∈y↔∃ww∈x∧∀yφ
34 elequ2 ⊢w=y→z∈w↔z∈y
35 nfa1 ⊢Ⅎy∀yφ
36 35 19.3 ⊢∀y∀yφ↔∀yφ
37 36 anbi2i ⊢w∈x∧∀y∀yφ↔w∈x∧∀yφ
38 37 exbii ⊢∃ww∈x∧∀y∀yφ↔∃ww∈x∧∀yφ
39 38 a1i ⊢w=y→∃ww∈x∧∀y∀yφ↔∃ww∈x∧∀yφ
40 34 39 bibi12d ⊢w=y→z∈w↔∃ww∈x∧∀y∀yφ↔z∈y↔∃ww∈x∧∀yφ
41 40 albidv ⊢w=y→∀zz∈w↔∃ww∈x∧∀y∀yφ↔∀zz∈y↔∃ww∈x∧∀yφ
42 8 33 41 cbvexv1 ⊢∃w∀zz∈w↔∃ww∈x∧∀y∀yφ↔∃y∀zz∈y↔∃ww∈x∧∀yφ
43 29 42 sylib ⊢∀w∃y∀z∀yφ→z=y→∃y∀zz∈y↔∃ww∈x∧∀yφ