Axiom ax-sep

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

It was derived as axsep above and is therefore redundant in ZF set theory, which contains ax-rep 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 x e. z , so that it asserts the existence of a collection only if it is smaller than some other collection z that already exists. This prevents Russell's paradox ru . In some texts, this scheme is called "Aussonderung" (German for "separation") or "Subset Axiom".

The variable x can occur in the formula ph , which in textbooks is often written ph ( x ) . To specify this in the Metamath language, weomit the distinct variable condition ($d) that x not occur in ph .

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

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

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

	Ref	Expression
Assertion	ax-sep	⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vy	⊢ 𝑦
1		vx	⊢ 𝑥
2	1	cv	⊢ 𝑥
3	0	cv	⊢ 𝑦
4	2 3	wcel	⊢ 𝑥 ∈ 𝑦
5		vz	⊢ 𝑧
6	5	cv	⊢ 𝑧
7	2 6	wcel	⊢ 𝑥 ∈ 𝑧
8		wph	⊢ 𝜑
9	7 8	wa	⊢ ( 𝑥 ∈ 𝑧 ∧ 𝜑 )
10	4 9	wb	⊢ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
11	10 1	wal	⊢ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
12	11 0	wex	⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )