ax-reg

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vy	⊢ 𝑦
1	0	cv	⊢ 𝑦
2		vx	⊢ 𝑥
3	2	cv	⊢ 𝑥
4	1 3	wcel	⊢ 𝑦 ∈ 𝑥
5	4 0	wex	⊢ ∃ 𝑦 𝑦 ∈ 𝑥
6		vz	⊢ 𝑧
7	6	cv	⊢ 𝑧
8	7 1	wcel	⊢ 𝑧 ∈ 𝑦
9	7 3	wcel	⊢ 𝑧 ∈ 𝑥
10	9	wn	⊢ ¬ 𝑧 ∈ 𝑥
11	8 10	wi	⊢ ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 )
12	11 6	wal	⊢ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 )
13	4 12	wa	⊢ ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) )
14	13 0	wex	⊢ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) )
15	5 14	wi	⊢ ( ∃ 𝑦 𝑦 ∈ 𝑥 → ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) )

Metamath Proof Explorer

Axiom ax-reg

Detailed syntax breakdown