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 4016. (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 1466 | . . . . 5 |
4 | va | . . . . . . 7 | |
5 | 1, 4 | wel 1466 | . . . . . 6 |
6 | wph | . . . . . 6 | |
7 | 5, 6 | wa 103 | . . . . 5 |
8 | 3, 7 | wb 104 | . . . 4 |
9 | 8, 1 | wal 1314 | . . 3 |
10 | 9, 2 | wex 1453 | . 2 |
11 | 10, 4 | wal 1314 | 1 |
Colors of variables: wff set class |
This axiom is referenced by: bdsep1 13010 |
Copyright terms: Public domain | W3C validator |