Axiom ax-reg 4576

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 4579) 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 4581). A stronger version that works for proper classes is proved as zfregs 4630.

Assertion

Ref	Expression
ax-reg	⊢ (∃y y ∈ x → ∃y(y ∈ x ⋀ ∀z(z ∈ y → ¬ z ∈ 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 954	. . . 4 class y
3		vx	. . . . 5 set x
4	3	cv 954	. . . 4 class x
5	2, 4	wcel 957	. . 3 wff y ∈ x
6	5, 1	wex 979	. 2 wff ∃y y ∈ x
7		vz	. . . . . . . 8 set z
8	7	cv 954	. . . . . . 7 class z
9	8, 2	wcel 957	. . . . . 6 wff z ∈ y
10	8, 4	wcel 957	. . . . . . 7 wff z ∈ x
11	10	wn 2	. . . . . 6 wff ¬ z ∈ x
12	9, 11	wi 3	. . . . 5 wff (z ∈ y → ¬ z ∈ x)
13	12, 7	wal 953	. . . 4 wff ∀z(z ∈ y → ¬ z ∈ x)
14	5, 13	wa 223	. . 3 wff (y ∈ x ⋀ ∀z(z ∈ y → ¬ z ∈ x))
15	14, 1	wex 979	. 2 wff ∃y(y ∈ x ⋀ ∀z(z ∈ y → ¬ z ∈ x))
16	6, 15	wi 3	1 wff (∃y y ∈ x → ∃y(y ∈ x ⋀ ∀z(z ∈ y → ¬ z ∈ x)))

This axiom is referenced by:  axreg 4577

Copyright terms: Public domain