# 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}\in {y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 axregndlem2 ${⊢}{x}\in {y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {x}\to ¬{w}\in {y}\right)\right)$
2 nfnae ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}$
3 nfnae ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}$
4 2 3 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\wedge ¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\right)$
5 nfnae ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}$
6 nfnae ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}$
7 5 6 nfan ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\wedge ¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\right)$
8 nfcvf ${⊢}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\to \underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{x}$
9 8 nfcrd ${⊢}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\to Ⅎ{z}\phantom{\rule{.4em}{0ex}}{w}\in {x}$
10 9 adantr ${⊢}\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\wedge ¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\right)\to Ⅎ{z}\phantom{\rule{.4em}{0ex}}{w}\in {x}$
11 nfcvf ${⊢}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{y}$
12 11 nfcrd ${⊢}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to Ⅎ{z}\phantom{\rule{.4em}{0ex}}{w}\in {y}$
13 12 nfnd ${⊢}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to Ⅎ{z}\phantom{\rule{.4em}{0ex}}¬{w}\in {y}$
14 13 adantl ${⊢}\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\wedge ¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\right)\to Ⅎ{z}\phantom{\rule{.4em}{0ex}}¬{w}\in {y}$
15 10 14 nfimd ${⊢}\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\wedge ¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\right)\to Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({w}\in {x}\to ¬{w}\in {y}\right)$
16 elequ1 ${⊢}{w}={z}\to \left({w}\in {x}↔{z}\in {x}\right)$
17 elequ1 ${⊢}{w}={z}\to \left({w}\in {y}↔{z}\in {y}\right)$
18 17 notbid ${⊢}{w}={z}\to \left(¬{w}\in {y}↔¬{z}\in {y}\right)$
19 16 18 imbi12d ${⊢}{w}={z}\to \left(\left({w}\in {x}\to ¬{w}\in {y}\right)↔\left({z}\in {x}\to ¬{z}\in {y}\right)\right)$
20 19 a1i ${⊢}\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\wedge ¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\right)\to \left({w}={z}\to \left(\left({w}\in {x}\to ¬{w}\in {y}\right)↔\left({z}\in {x}\to ¬{z}\in {y}\right)\right)\right)$
21 7 15 20 cbvald ${⊢}\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\wedge ¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\right)\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {x}\to ¬{w}\in {y}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)\right)$
22 21 anbi2d ${⊢}\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\wedge ¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\right)\to \left(\left({x}\in {y}\wedge \forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {x}\to ¬{w}\in {y}\right)\right)↔\left({x}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)\right)\right)$
23 4 22 exbid ${⊢}\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\wedge ¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {x}\to ¬{w}\in {y}\right)\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)\right)\right)$
24 1 23 syl5ib ${⊢}\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\wedge ¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\right)\to \left({x}\in {y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)\right)\right)$
25 24 ex ${⊢}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\to \left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \left({x}\in {y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)\right)\right)\right)$
26 axregndlem1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \left({x}\in {y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)\right)\right)$
27 26 aecoms ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\to \left({x}\in {y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)\right)\right)$
28 19.8a ${⊢}{x}\in {y}\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {y}$
29 nfae ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}$
30 elirrv ${⊢}¬{z}\in {z}$
31 elequ2 ${⊢}{z}={y}\to \left({z}\in {z}↔{z}\in {y}\right)$
32 30 31 mtbii ${⊢}{z}={y}\to ¬{z}\in {y}$
33 32 a1d ${⊢}{z}={y}\to \left({z}\in {x}\to ¬{z}\in {y}\right)$
34 33 alimi ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)$
35 34 anim2i ${⊢}\left({x}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\right)\to \left({x}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)\right)$
36 35 expcom ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \left({x}\in {y}\to \left({x}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)\right)\right)$
37 29 36 eximd ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)\right)\right)$
38 28 37 syl5 ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \left({x}\in {y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)\right)\right)$
39 25 27 38 pm2.61ii ${⊢}{x}\in {y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)\right)$