Theorem nalset

Description: No set contains all sets. Theorem 41 of Suppes p. 30. (Contributed by NM, 23-Aug-1993) Remove use of ax-12 and ax-13 . (Revised by BJ, 31-May-2019)

	Ref	Expression
Assertion	nalset	$$⊢\neg \exists x\forall yy\in x$$

Proof

Step	Hyp	Ref	Expression
1		alexn	$$⊢\forall x\exists y\neg y\in x\leftrightarrow \neg \exists x\forall yy\in x$$
2		ax-sep	$$⊢\exists y\forall z\left(z\in y\leftrightarrow \left(z\in x\wedge \neg z\in z\right)\right)$$
3		elequ1	$$⊢z=y\to \left(z\in y\leftrightarrow y\in y\right)$$
4		elequ1	$$⊢z=y\to \left(z\in x\leftrightarrow y\in x\right)$$
5		elequ1	$$⊢z=y\to \left(z\in z\leftrightarrow y\in z\right)$$
6		elequ2	$$⊢z=y\to \left(y\in z\leftrightarrow y\in y\right)$$
7	5 6	bitrd	$$⊢z=y\to \left(z\in z\leftrightarrow y\in y\right)$$
8	7	notbid	$$⊢z=y\to \left(\neg z\in z\leftrightarrow \neg y\in y\right)$$
9	4 8	anbi12d	$$⊢z=y\to \left(\left(z\in x\wedge \neg z\in z\right)\leftrightarrow \left(y\in x\wedge \neg y\in y\right)\right)$$
10	3 9	bibi12d	$$⊢z=y\to \left(\left(z\in y\leftrightarrow \left(z\in x\wedge \neg z\in z\right)\right)\leftrightarrow \left(y\in y\leftrightarrow \left(y\in x\wedge \neg y\in y\right)\right)\right)$$
11	10	spvv	$$⊢\forall z\left(z\in y\leftrightarrow \left(z\in x\wedge \neg z\in z\right)\right)\to \left(y\in y\leftrightarrow \left(y\in x\wedge \neg y\in y\right)\right)$$
12		pclem6	$$⊢\left(y\in y\leftrightarrow \left(y\in x\wedge \neg y\in y\right)\right)\to \neg y\in x$$
13	11 12	syl	$$⊢\forall z\left(z\in y\leftrightarrow \left(z\in x\wedge \neg z\in z\right)\right)\to \neg y\in x$$
14	2 13	eximii	$$⊢\exists y\neg y\in x$$
15	1 14	mpgbi	$$⊢\neg \exists x\forall yy\in x$$