Axiom ax-reg 9570

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

Assertion

Ref	Expression
ax-reg	⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Axiom ax-reg

Step	Hyp	Ref	Expression
1		vy	. . . 4 setvar 𝑦
2		vx	. . . 4 setvar 𝑥
3	1, 2	wel 2146	. . 3 wff 𝑦 ∈ 𝑥
4	3, 1	wex 1812	. 2 wff ∃𝑦 𝑦 ∈ 𝑥
5		vz	. . . . . . 7 setvar 𝑧
6	5, 1	wel 2146	. . . . . 6 wff 𝑧 ∈ 𝑦
7	5, 2	wel 2146	. . . . . . 7 wff 𝑧 ∈ 𝑥
8	7	wn 3	. . . . . 6 wff ¬ 𝑧 ∈ 𝑥
9	6, 8	wi 4	. . . . 5 wff (𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)
10	9, 5	wal 1568	. . . 4 wff ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)
11	3, 10	wa 401	. . 3 wff (𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥))
12	11, 1	wex 1812	. 2 wff ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥))
13	4, 12	wi 4	1 wff (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))

This axiom is used by:  axreg2  9571  zfregcl  9572  elirrv  9575  elirrvOLD  9576  axnulregtco  37238