![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > Mathboxes > ax-bdsep | GIF version |
Description: Axiom scheme of bounded (or restricted, or Δ0) 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 3978. (Contributed by BJ, 5-Oct-2019.) |
Ref | Expression |
---|---|
ax-bdsep.1 | ⊢ BOUNDED 𝜑 |
Ref | Expression |
---|---|
ax-bdsep | ⊢ ∀𝑎∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . . . . 6 setvar 𝑥 | |
2 | vb | . . . . . 6 setvar 𝑏 | |
3 | 1, 2 | wel 1446 | . . . . 5 wff 𝑥 ∈ 𝑏 |
4 | va | . . . . . . 7 setvar 𝑎 | |
5 | 1, 4 | wel 1446 | . . . . . 6 wff 𝑥 ∈ 𝑎 |
6 | wph | . . . . . 6 wff 𝜑 | |
7 | 5, 6 | wa 103 | . . . . 5 wff (𝑥 ∈ 𝑎 ∧ 𝜑) |
8 | 3, 7 | wb 104 | . . . 4 wff (𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)) |
9 | 8, 1 | wal 1294 | . . 3 wff ∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)) |
10 | 9, 2 | wex 1433 | . 2 wff ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)) |
11 | 10, 4 | wal 1294 | 1 wff ∀𝑎∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)) |
Colors of variables: wff set class |
This axiom is referenced by: bdsep1 12500 |
Copyright terms: Public domain | W3C validator |