# Metamath Proof Explorer

## Theorem axregndlem1

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) (New usage is discouraged.)

Ref Expression
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 19.8a ${⊢}{x}\in {y}\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {y}$
2 nfae ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}$
3 nfae ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}$
4 elirrv ${⊢}¬{x}\in {x}$
5 elequ1 ${⊢}{x}={z}\to \left({x}\in {x}↔{z}\in {x}\right)$
6 4 5 mtbii ${⊢}{x}={z}\to ¬{z}\in {x}$
7 6 sps ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to ¬{z}\in {x}$
8 7 pm2.21d ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \left({z}\in {x}\to ¬{z}\in {y}\right)$
9 3 8 alrimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)$
10 9 anim2i ${⊢}\left({x}\in {y}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \left({x}\in {y}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to ¬{z}\in {y}\right)\right)$
11 10 expcom ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\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)$
12 2 11 eximd ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\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)$
13 1 12 syl5 ${⊢}\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)$