# Metamath Proof Explorer

## Theorem axregndlem2

Description: Lemma for 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 Mario Carneiro, 10-Dec-2016) (New usage is discouraged.)

Ref Expression
Assertion axregndlem2 ${⊢}{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 axreg2 ${⊢}{w}\in {y}\to \exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\to ¬{z}\in {y}\right)\right)$
2 1 ax-gen ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\to \exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\to ¬{z}\in {y}\right)\right)\right)$
3 nfnae ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
4 nfnae ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}$
5 3 4 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)$
6 nfcvd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{w}$
7 nfcvf ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
8 7 adantr ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
9 6 8 nfeld ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{w}\in {y}$
10 nfv ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)$
11 nfnae ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
12 nfnae ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}$
13 11 12 nfan ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)$
14 nfcvf ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{z}$
15 14 adantl ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{z}$
16 15 6 nfeld ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\in {w}$
17 15 8 nfeld ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\in {y}$
18 17 nfnd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬{z}\in {y}$
19 16 18 nfimd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\to ¬{z}\in {y}\right)$
20 13 19 nfald ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\to ¬{z}\in {y}\right)$
21 9 20 nfand ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\to ¬{z}\in {y}\right)\right)$
22 10 21 nfexd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\to ¬{z}\in {y}\right)\right)$
23 9 22 nfimd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\to \exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\to ¬{z}\in {y}\right)\right)\right)$
24 simpr ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to {w}={x}$
25 24 eleq1d ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left({w}\in {y}↔{x}\in {y}\right)$
26 nfcvd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{w}$
27 nfcvf2 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{x}$
28 27 adantl ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{x}$
29 26 28 nfeqd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{z}\phantom{\rule{.4em}{0ex}}{w}={x}$
30 13 29 nfan1 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)$
31 24 eleq2d ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left({z}\in {w}↔{z}\in {x}\right)$
32 31 imbi1d ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left(\left({z}\in {w}\to ¬{z}\in {y}\right)↔\left({z}\in {x}\to ¬{z}\in {y}\right)\right)$
33 30 32 albid ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\to ¬{z}\in {y}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)\right)$
34 25 33 anbi12d ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left(\left({w}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\to ¬{z}\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)$
35 34 ex ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \left({w}={x}\to \left(\left({w}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\to ¬{z}\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)\right)$
36 5 21 35 cbvexd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \left(\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\to ¬{z}\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)$
37 36 adantr ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left(\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\to ¬{z}\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)$
38 25 37 imbi12d ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left(\left({w}\in {y}\to \exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\to ¬{z}\in {y}\right)\right)\right)↔\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)$
39 38 ex ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \left({w}={x}\to \left(\left({w}\in {y}\to \exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\to ¬{z}\in {y}\right)\right)\right)↔\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)\right)$
40 5 23 39 cbvald ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\to \exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}\to ¬{z}\in {y}\right)\right)\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\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)$
41 2 40 mpbii ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\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)$
42 41 19.21bi ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\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)$
43 42 ex ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(¬\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)\right)$
44 elirrv ${⊢}¬{x}\in {x}$
45 elequ2 ${⊢}{x}={y}\to \left({x}\in {x}↔{x}\in {y}\right)$
46 44 45 mtbii ${⊢}{x}={y}\to ¬{x}\in {y}$
47 46 sps ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to ¬{x}\in {y}$
48 47 pm2.21d ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={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)$
49 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)$
50 43 48 49 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)$