Axiom ax-reg 1078

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

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(s):   x,y,z

Detailed syntax breakdown of Axiom ax-reg

Step	Hyp	Ref	Expression
1		vy	. . . 4 set y
2		vx	. . . 4 set x
3	1, 2	wel 803	. . 3 wff y e. x
4	3, 1	wex 678	. 2 wff E.y y e. x
5		vz	. . . . . . 7 set z
6	5, 1	wel 803	. . . . . 6 wff z e. y
7	5, 2	wel 803	. . . . . . 7 wff z e. x
8	7	wn 1	. . . . . 6 wff -. z e. x
9	6, 8	wi 2	. . . . 5 wff (z e. y -> -. z e. x)
10	9, 5	wal 672	. . . 4 wff A.z(z e. y -> -. z e. x)
11	3, 10	wa 196	. . 3 wff (y e. x /\ A.z(z e. y -> -. z e. x))
12	11, 1	wex 678	. 2 wff E.y(y e. x /\ A.z(z e. y -> -. z e. x))
13	4, 12	wi 2	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 1083

metamath.org