Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > Mathboxes > ax-bdsep | Unicode 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 4094. (Contributed by BJ, 5-Oct-2019.) |
Ref | Expression |
---|---|
ax-bdsep.1 | BOUNDED |
Ref | Expression |
---|---|
ax-bdsep |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . . . . 6 | |
2 | vb | . . . . . 6 | |
3 | 1, 2 | wel 2136 | . . . . 5 |
4 | va | . . . . . . 7 | |
5 | 1, 4 | wel 2136 | . . . . . 6 |
6 | wph | . . . . . 6 | |
7 | 5, 6 | wa 103 | . . . . 5 |
8 | 3, 7 | wb 104 | . . . 4 |
9 | 8, 1 | wal 1340 | . . 3 |
10 | 9, 2 | wex 1479 | . 2 |
11 | 10, 4 | wal 1340 | 1 |
Colors of variables: wff set class |
This axiom is referenced by: bdsep1 13602 |
Copyright terms: Public domain | W3C validator |