Metamath Proof Explorer


Axiom 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 ( ∃ 𝑦 𝑦𝑥 → ∃ 𝑦 ( 𝑦𝑥 ∧ ∀ 𝑧 ( 𝑧𝑦 → ¬ 𝑧𝑥 ) ) )