Axiom ax-reg 4593

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 4596) that every non-empty set contains a set disjoint from itself. One consequence is that it denies the existence of a set containing itself (elirrv 4598). A stronger version that works for proper classes is proved as zfregs 4647.

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	. . . . 5 set y
2	1	cv 955	. . . 4 class y
3		vx	. . . . 5 set x
4	3	cv 955	. . . 4 class x
5	2, 4	wcel 958	. . 3 wff y e. x
6	5, 1	wex 980	. 2 wff E.y y e. x
7		vz	. . . . . . . 8 set z
8	7	cv 955	. . . . . . 7 class z
9	8, 2	wcel 958	. . . . . 6 wff z e. y
10	8, 4	wcel 958	. . . . . . 7 wff z e. x
11	10	wn 2	. . . . . 6 wff -. z e. x
12	9, 11	wi 3	. . . . 5 wff (z e. y -> -. z e. x)
13	12, 7	wal 954	. . . 4 wff A.z(z e. y -> -. z e. x)
14	5, 13	wa 223	. . 3 wff (y e. x /\ A.z(z e. y -> -. z e. x))
15	14, 1	wex 980	. 2 wff E.y(y e. x /\ A.z(z e. y -> -. z e. x))
16	6, 15	wi 3	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:  axreg 4594

Copyright terms: Public domain