Metamath Proof Explorer

Theorem axregnd

Description: A version of the Axiom of Regularity with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Jan-2002) (Proof shortened by Wolf Lammen, 18-Aug-2019) (New usage is discouraged.)

Ref Expression
Assertion axregnd ⊢x∈y→∃xx∈y∧∀zz∈x→¬z∈y

Proof

Step Hyp Ref Expression
1 axregndlem2 ⊢x∈y→∃xx∈y∧∀ww∈x→¬w∈y
2 nfnae ⊢Ⅎx¬∀zz=x
3 nfnae ⊢Ⅎx¬∀zz=y
4 2 3 nfan ⊢Ⅎx¬∀zz=x∧¬∀zz=y
5 nfnae ⊢Ⅎz¬∀zz=x
6 nfnae ⊢Ⅎz¬∀zz=y
7 5 6 nfan ⊢Ⅎz¬∀zz=x∧¬∀zz=y
8 nfcvf ⊢¬∀zz=x→Ⅎ_zx
9 8 nfcrd ⊢¬∀zz=x→Ⅎzw∈x
10 9 adantr ⊢¬∀zz=x∧¬∀zz=y→Ⅎzw∈x
11 nfcvf ⊢¬∀zz=y→Ⅎ_zy
12 11 nfcrd ⊢¬∀zz=y→Ⅎzw∈y
13 12 nfnd ⊢¬∀zz=y→Ⅎz¬w∈y
14 13 adantl ⊢¬∀zz=x∧¬∀zz=y→Ⅎz¬w∈y
15 10 14 nfimd ⊢¬∀zz=x∧¬∀zz=y→Ⅎzw∈x→¬w∈y
16 elequ1 ⊢w=z→w∈x↔z∈x
17 elequ1 ⊢w=z→w∈y↔z∈y
18 17 notbid ⊢w=z→¬w∈y↔¬z∈y
19 16 18 imbi12d ⊢w=z→w∈x→¬w∈y↔z∈x→¬z∈y
20 19 a1i ⊢¬∀zz=x∧¬∀zz=y→w=z→w∈x→¬w∈y↔z∈x→¬z∈y
21 7 15 20 cbvald ⊢¬∀zz=x∧¬∀zz=y→∀ww∈x→¬w∈y↔∀zz∈x→¬z∈y
22 21 anbi2d ⊢¬∀zz=x∧¬∀zz=y→x∈y∧∀ww∈x→¬w∈y↔x∈y∧∀zz∈x→¬z∈y
23 4 22 exbid ⊢¬∀zz=x∧¬∀zz=y→∃xx∈y∧∀ww∈x→¬w∈y↔∃xx∈y∧∀zz∈x→¬z∈y
24 1 23 imbitrid ⊢¬∀zz=x∧¬∀zz=y→x∈y→∃xx∈y∧∀zz∈x→¬z∈y
25 24 ex ⊢¬∀zz=x→¬∀zz=y→x∈y→∃xx∈y∧∀zz∈x→¬z∈y
26 axregndlem1 ⊢∀xx=z→x∈y→∃xx∈y∧∀zz∈x→¬z∈y
27 26 aecoms ⊢∀zz=x→x∈y→∃xx∈y∧∀zz∈x→¬z∈y
28 19.8a ⊢x∈y→∃xx∈y
29 nfae ⊢Ⅎx∀zz=y
30 elirrv ⊢¬z∈z
31 elequ2 ⊢z=y→z∈z↔z∈y
32 30 31 mtbii ⊢z=y→¬z∈y
33 32 a1d ⊢z=y→z∈x→¬z∈y
34 33 alimi ⊢∀zz=y→∀zz∈x→¬z∈y
35 34 anim2i ⊢x∈y∧∀zz=y→x∈y∧∀zz∈x→¬z∈y
36 35 expcom ⊢∀zz=y→x∈y→x∈y∧∀zz∈x→¬z∈y
37 29 36 eximd ⊢∀zz=y→∃xx∈y→∃xx∈y∧∀zz∈x→¬z∈y
38 28 37 syl5 ⊢∀zz=y→x∈y→∃xx∈y∧∀zz∈x→¬z∈y
39 25 27 38 pm2.61ii ⊢x∈y→∃xx∈y∧∀zz∈x→¬z∈y