Metamath Proof Explorer

Theorem axrepndlem1

Description: Lemma for the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jan-2002) (New usage is discouraged.)

Ref Expression
Assertion axrepndlem1 ⊢¬∀yy=z→∃x∃y∀zφ→z=y→∀zz∈x↔∃xx∈y∧∀yφ

Proof

Step Hyp Ref Expression
1 axrep2 ⊢∃x∃y∀wwzφ→w=y→∀ww∈x↔∃xx∈y∧∀ywzφ
2 nfnae ⊢Ⅎx¬∀yy=z
3 nfnae ⊢Ⅎy¬∀yy=z
4 nfnae ⊢Ⅎz¬∀yy=z
5 nfs1v ⊢Ⅎzwzφ
6 5 a1i ⊢¬∀yy=z→Ⅎzwzφ
7 nfcvd ⊢¬∀yy=z→Ⅎ_zw
8 nfcvf2 ⊢¬∀yy=z→Ⅎ_zy
9 7 8 nfeqd ⊢¬∀yy=z→Ⅎzw=y
10 6 9 nfimd ⊢¬∀yy=z→Ⅎzwzφ→w=y
11 sbequ12r ⊢w=z→wzφ↔φ
12 equequ1 ⊢w=z→w=y↔z=y
13 11 12 imbi12d ⊢w=z→wzφ→w=y↔φ→z=y
14 13 a1i ⊢¬∀yy=z→w=z→wzφ→w=y↔φ→z=y
15 4 10 14 cbvald ⊢¬∀yy=z→∀wwzφ→w=y↔∀zφ→z=y
16 3 15 exbid ⊢¬∀yy=z→∃y∀wwzφ→w=y↔∃y∀zφ→z=y
17 nfvd ⊢¬∀yy=z→Ⅎzw∈x
18 8 nfcrd ⊢¬∀yy=z→Ⅎzx∈y
19 3 6 nfald ⊢¬∀yy=z→Ⅎz∀ywzφ
20 18 19 nfand ⊢¬∀yy=z→Ⅎzx∈y∧∀ywzφ
21 2 20 nfexd ⊢¬∀yy=z→Ⅎz∃xx∈y∧∀ywzφ
22 17 21 nfbid ⊢¬∀yy=z→Ⅎzw∈x↔∃xx∈y∧∀ywzφ
23 elequ1 ⊢w=z→w∈x↔z∈x
24 23 adantl ⊢¬∀yy=z∧w=z→w∈x↔z∈x
25 nfeqf2 ⊢¬∀yy=z→Ⅎyw=z
26 3 25 nfan1 ⊢Ⅎy¬∀yy=z∧w=z
27 11 adantl ⊢¬∀yy=z∧w=z→wzφ↔φ
28 26 27 albid ⊢¬∀yy=z∧w=z→∀ywzφ↔∀yφ
29 28 anbi2d ⊢¬∀yy=z∧w=z→x∈y∧∀ywzφ↔x∈y∧∀yφ
30 29 exbidv ⊢¬∀yy=z∧w=z→∃xx∈y∧∀ywzφ↔∃xx∈y∧∀yφ
31 24 30 bibi12d ⊢¬∀yy=z∧w=z→w∈x↔∃xx∈y∧∀ywzφ↔z∈x↔∃xx∈y∧∀yφ
32 31 ex ⊢¬∀yy=z→w=z→w∈x↔∃xx∈y∧∀ywzφ↔z∈x↔∃xx∈y∧∀yφ
33 4 22 32 cbvald ⊢¬∀yy=z→∀ww∈x↔∃xx∈y∧∀ywzφ↔∀zz∈x↔∃xx∈y∧∀yφ
34 16 33 imbi12d ⊢¬∀yy=z→∃y∀wwzφ→w=y→∀ww∈x↔∃xx∈y∧∀ywzφ↔∃y∀zφ→z=y→∀zz∈x↔∃xx∈y∧∀yφ
35 2 34 exbid ⊢¬∀yy=z→∃x∃y∀wwzφ→w=y→∀ww∈x↔∃xx∈y∧∀ywzφ↔∃x∃y∀zφ→z=y→∀zz∈x↔∃xx∈y∧∀yφ
36 1 35 mpbii ⊢¬∀yy=z→∃x∃y∀zφ→z=y→∀zz∈x↔∃xx∈y∧∀yφ