![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ax-sep | Structured version Visualization version GIF version |
Description: Axiom scheme of
separation. This is an axiom scheme of Zermelo and
Zermelo-Fraenkel set theories.
It was derived as axsep 5296 above and is therefore redundant in ZF set theory, which contains ax-rep 5283 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 3774. 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 5299, 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 5359 shows (showing the necessity of that condition in zfauscl 5299). Scheme Sep of [BellMachover] p. 463. (Contributed by NM, 11-Sep-2006.) |
Ref | Expression |
---|---|
ax-sep | ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . . . 5 setvar 𝑥 | |
2 | vy | . . . . 5 setvar 𝑦 | |
3 | 1, 2 | wel 2108 | . . . 4 wff 𝑥 ∈ 𝑦 |
4 | vz | . . . . . 6 setvar 𝑧 | |
5 | 1, 4 | wel 2108 | . . . . 5 wff 𝑥 ∈ 𝑧 |
6 | wph | . . . . 5 wff 𝜑 | |
7 | 5, 6 | wa 397 | . . . 4 wff (𝑥 ∈ 𝑧 ∧ 𝜑) |
8 | 3, 7 | wb 205 | . . 3 wff (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) |
9 | 8, 1 | wal 1540 | . 2 wff ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) |
10 | 9, 2 | wex 1782 | 1 wff ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) |
Colors of variables: wff setvar class |
This axiom is referenced by: axsepg 5298 zfauscl 5299 bm1.3ii 5300 ax6vsep 5301 axnul 5303 nalset 5311 bj-zfauscl 35741 bj-bm1.3ii 35882 |
Copyright terms: Public domain | W3C validator |