This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ∃ y y ∈ x → ∃ y y ∈ x ∧ ∀ z z ∈ y → ¬ z ∈ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 vy setvar y
1 0 cv setvar y
2 vx setvar x
3 2 cv setvar x
4 1 3 wcel wff y ∈ x
5 4 0 wex wff ∃ y y ∈ x
6 vz setvar z
7 6 cv setvar z
8 7 1 wcel wff z ∈ y
9 7 3 wcel wff z ∈ x
10 9 wn wff ¬ z ∈ x
11 8 10 wi wff z ∈ y → ¬ z ∈ x
12 11 6 wal wff ∀ z z ∈ y → ¬ z ∈ x
13 4 12 wa wff y ∈ x ∧ ∀ z z ∈ y → ¬ z ∈ x
14 13 0 wex wff ∃ y y ∈ x ∧ ∀ z z ∈ y → ¬ z ∈ x
15 5 14 wi wff ∃ y y ∈ x → ∃ y y ∈ x ∧ ∀ z z ∈ y → ¬ z ∈ x