Axiom ax-bdsep 13766

Description: Axiom scheme of bounded (or restricted, or Δ₀) separation. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. For the full axiom of separation, see ax-sep 4100. (Contributed by BJ, 5-Oct-2019.)

Hypothesis

Ref	Expression
ax-bdsep.1	⊢ BOUNDED 𝜑

Assertion

Ref	Expression
ax-bdsep	⊢ ∀𝑎∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))

Distinct variable groups:   𝑎,𝑏,𝑥   𝜑,𝑎,𝑏

Allowed substitution hint:   𝜑(𝑥)

Detailed syntax breakdown of Axiom ax-bdsep

Step	Hyp	Ref	Expression
1		vx	. . . . . 6 setvar 𝑥
2		vb	. . . . . 6 setvar 𝑏
3	1, 2	wel 2137	. . . . 5 wff 𝑥 ∈ 𝑏
4		va	. . . . . . 7 setvar 𝑎
5	1, 4	wel 2137	. . . . . 6 wff 𝑥 ∈ 𝑎
6		wph	. . . . . 6 wff 𝜑
7	5, 6	wa 103	. . . . 5 wff (𝑥 ∈ 𝑎 ∧ 𝜑)
8	3, 7	wb 104	. . . 4 wff (𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))
9	8, 1	wal 1341	. . 3 wff ∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))
10	9, 2	wex 1480	. 2 wff ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))
11	10, 4	wal 1341	1 wff ∀𝑎∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))

This axiom is referenced by:  bdsep1  13767