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	|- ( E. y y e. x -> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vy	|- y
1	0	cv	|- y
2		vx	|- x
3	2	cv	|- x
4	1 3	wcel	|- y e. x
5	4 0	wex	|- E. y y e. x
6		vz	|- z
7	6	cv	|- z
8	7 1	wcel	|- z e. y
9	7 3	wcel	|- z e. x
10	9	wn	|- -. z e. x
11	8 10	wi	|- ( z e. y -> -. z e. x )
12	11 6	wal	|- A. z ( z e. y -> -. z e. x )
13	4 12	wa	|- ( y e. x /\ A. z ( z e. y -> -. z e. x ) )
14	13 0	wex	|- E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) )
15	5 14	wi	|- ( E. y y e. x -> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) )