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	⊢ (∃y y ∈ x → ∃y(y ∈ x ∧ ∀z(z ∈ y → ¬ z ∈ 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 ∈ x
4	3, 1	wex 678	. 2 wff ∃y y ∈ x
5		vz	. . . . . . 7 set z
6	5, 1	wel 803	. . . . . 6 wff z ∈ y
7	5, 2	wel 803	. . . . . . 7 wff z ∈ x
8	7	wn 1	. . . . . 6 wff ¬ z ∈ x
9	6, 8	wi 2	. . . . 5 wff (z ∈ y → ¬ z ∈ x)
10	9, 5	wal 672	. . . 4 wff ∀z(z ∈ y → ¬ z ∈ x)
11	3, 10	wa 196	. . 3 wff (y ∈ x ∧ ∀z(z ∈ y → ¬ z ∈ x))
12	11, 1	wex 678	. 2 wff ∃y(y ∈ x ∧ ∀z(z ∈ y → ¬ z ∈ x))
13	4, 12	wi 2	1 wff (∃y y ∈ x → ∃y(y ∈ x ∧ ∀z(z ∈ y → ¬ z ∈ x)))

This axiom is referenced by:  axreg 1083

metamath.org