Axiom ax-sep 5255

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

It was derived as axsep 5254 above and is therefore redundant in ZF set theory, which contains ax-rep 5236 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 3741. 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 sepg 5257, 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 notsep 5332 shows (showing the necessity of that condition in sepgi 5258, hence in sepg 5257 and ax-sep 5255).

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

Step	Hyp	Ref	Expression
1		vx	. . . . 5 setvar 𝑥
2		vy	. . . . 5 setvar 𝑦
3	1, 2	wel 2146	. . . 4 wff 𝑥 ∈ 𝑦
4		vz	. . . . . 6 setvar 𝑧
5	1, 4	wel 2146	. . . . 5 wff 𝑥 ∈ 𝑧
6		wph	. . . . 5 wff 𝜑
7	5, 6	wa 401	. . . 4 wff (𝑥 ∈ 𝑧 ∧ 𝜑)
8	3, 7	wb 209	. . 3 wff (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
9	8, 1	wal 1568	. 2 wff ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
10	9, 2	wex 1812	1 wff ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))

This axiom is used by:  axsepg  5256  sepg  5257  zfausclOLD  5259  sepexlem  5260  bm1.3iiOLD  5263  ax6vsep  5264  axnul  5266  exnelv  5274  nalsetOLD  5276  axsepg2  35653  axsepg3  35654  axsepg3ALT  35655  bj-sepg  37654  bj-bm1.3ii  37795  ssclaxsep  45792