Axiom ax-reg 8497

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 8500) that every nonempty set contains a set disjoint from itself. One consequence is that it denies the existence of a set containing itself (elirrv 8504). A stronger version that works for proper classes is proved as zfregs 8608. (Contributed by NM, 14-Aug-1993.)

Assertion

Ref	Expression
ax-reg	|- ( E. y y e. x -> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) )

Distinct variable group:   x, y, z

Detailed syntax breakdown of Axiom ax-reg

Step	Hyp	Ref	Expression
1		vy	. . . 4 setvar y
2		vx	. . . 4 setvar x
3	1, 2	wel 1991	. . 3 wff y e. x
4	3, 1	wex 1704	. 2 wff E. y y e. x
5		vz	. . . . . . 7 setvar z
6	5, 1	wel 1991	. . . . . 6 wff z e. y
7	5, 2	wel 1991	. . . . . . 7 wff z e. x
8	7	wn 3	. . . . . 6 wff -. z e. x
9	6, 8	wi 4	. . . . 5 wff ( z e. y -> -. z e. x )
10	9, 5	wal 1481	. . . 4 wff A. z ( z e. y -> -. z e. x )
11	3, 10	wa 384	. . 3 wff ( y e. x /\ A. z ( z e. y -> -. z e. x ) )
12	11, 1	wex 1704	. 2 wff E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) )
13	4, 12	wi 4	1 wff ( E. y y e. x -> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) )

This axiom is referenced by:  axreg2  8498