MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-sep Structured version   Visualization version   GIF version

Axiom ax-sep 5224
Description: Axiom scheme of separation. This is an axiom scheme of Zermelo and Zermelo-Fraenkel set theories.

It was derived as axsep 5223 above and is therefore redundant in ZF set theory, which contains ax-rep 5210 as an axiom (contrary to Zermelo set theory). We state it as a separate axiom here so that some of its uses can be identified more easily. Some textbooks present the axiom scheme of separation as a separate axiom scheme in order to show that much of set theory can be derived without the stronger axiom scheme of replacement (which is not part of Zermelo set theory).

The axiom scheme of separation is a weak form of Frege's axiom scheme of (unrestricted) comprehension, in that it conditions it with the condition 𝑥𝑧, so that it asserts the existence of a collection only if it is smaller than some other collection 𝑧 that already exists. This prevents Russell's paradox ru 3716. In some texts, this scheme is called "Aussonderung" (German for "separation") or "Subset Axiom".

The variable 𝑥 can occur in the formula 𝜑, which in textbooks is often written 𝜑(𝑥). To specify this in the Metamath language, we omit the distinct variable condition ($d) that 𝑥 not occur in 𝜑.

For a version using a class variable, see zfauscl 5226, which requires the axiom of extensionality as well as the axiom scheme of separation for its derivation.

If we omit the requirement that 𝑦 not occur in 𝜑, we can derive a contradiction, as notzfaus 5286 shows (showing the necessity of that condition in zfauscl 5226).

Scheme Sep of [BellMachover] p. 463. (Contributed by NM, 11-Sep-2006.)

Assertion
Ref Expression
ax-sep 𝑦𝑥(𝑥𝑦 ↔ (𝑥𝑧𝜑))
Distinct variable groups:   𝑥,𝑦,𝑧   𝜑,𝑦,𝑧
Allowed substitution hint:   𝜑(𝑥)

Detailed syntax breakdown of Axiom ax-sep
StepHypRef Expression
1 vx . . . . 5 setvar 𝑥
2 vy . . . . 5 setvar 𝑦
31, 2wel 2108 . . . 4 wff 𝑥𝑦
4 vz . . . . . 6 setvar 𝑧
51, 4wel 2108 . . . . 5 wff 𝑥𝑧
6 wph . . . . 5 wff 𝜑
75, 6wa 396 . . . 4 wff (𝑥𝑧𝜑)
83, 7wb 205 . . 3 wff (𝑥𝑦 ↔ (𝑥𝑧𝜑))
98, 1wal 1537 . 2 wff 𝑥(𝑥𝑦 ↔ (𝑥𝑧𝜑))
109, 2wex 1782 1 wff 𝑦𝑥(𝑥𝑦 ↔ (𝑥𝑧𝜑))
Colors of variables: wff setvar class
This axiom is referenced by:  axsepg  5225  zfauscl  5226  bm1.3ii  5227  ax6vsep  5228  axnul  5230  nalset  5238  bj-zfauscl  35121  bj-bm1.3ii  35244
  Copyright terms: Public domain W3C validator