Axiom ax-sep 2718

Description: The Axiom of Separation of ZF set theory. It was derived as axsep 2717 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily.

Assertion

Ref	Expression
ax-sep	⊢ ∃y∀x(x ∈ y ↔ (x ∈ z ⋀ φ))

Distinct variable groups:   x,y,z   φ,y,z

Detailed syntax breakdown of Axiom ax-sep

Step	Hyp	Ref	Expression
1		vx	. . . . . 6 set x
2	1	cv 959	. . . . 5 class x
3		vy	. . . . . 6 set y
4	3	cv 959	. . . . 5 class y
5	2, 4	wcel 962	. . . 4 wff x ∈ y
6		vz	. . . . . . 7 set z
7	6	cv 959	. . . . . 6 class z
8	2, 7	wcel 962	. . . . 5 wff x ∈ z
9		wph	. . . . 5 wff φ
10	8, 9	wa 223	. . . 4 wff (x ∈ z ⋀ φ)
11	5, 10	wb 146	. . 3 wff (x ∈ y ↔ (x ∈ z ⋀ φ))
12	11, 1	wal 958	. 2 wff ∀x(x ∈ y ↔ (x ∈ z ⋀ φ))
13	12, 3	wex 984	1 wff ∃y∀x(x ∈ y ↔ (x ∈ z ⋀ φ))

This axiom is referenced by:  axsep2 2719  zfauscl 2720  bm1.3ii 2721  axnul 2724

Copyright terms: Public domain