Axiom ax-reg

Description: Axiom of Regularity. An axiom of Zermelo-Fraenkel set theory. Also called the Axiom of Foundation. A rather non-intuitive axiom that denies more than it asserts, it states (in the form of zfreg ) that every nonempty set contains a set disjoint from itself. One consequence is that it denies the existence of a set containing itself ( elirrv ). A stronger version that works for proper classes is proved as zfregs . (Contributed by NM, 14-Aug-1993)

	Ref	Expression
Assertion	ax-reg	$$⊢\exists yy\in x\to \exists y\left(y\in x\wedge \forall z\left(z\in y\to \neg z\in x\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vy	$$setvary$$
1	0	cv	$$setvary$$
2		vx	$$setvarx$$
3	2	cv	$$setvarx$$
4	1 3	wcel	$$wffy\in x$$
5	4 0	wex	$$wff\exists yy\in x$$
6		vz	$$setvarz$$
7	6	cv	$$setvarz$$
8	7 1	wcel	$$wffz\in y$$
9	7 3	wcel	$$wffz\in x$$
10	9	wn	$$wff\neg z\in x$$
11	8 10	wi	$$wff\left(z\in y\to \neg z\in x\right)$$
12	11 6	wal	$$wff\forall z\left(z\in y\to \neg z\in x\right)$$
13	4 12	wa	$$wff\left(y\in x\wedge \forall z\left(z\in y\to \neg z\in x\right)\right)$$
14	13 0	wex	$$wff\exists y\left(y\in x\wedge \forall z\left(z\in y\to \neg z\in x\right)\right)$$
15	5 14	wi	$$wff\left(\exists yy\in x\to \exists y\left(y\in x\wedge \forall z\left(z\in y\to \neg z\in x\right)\right)\right)$$