| Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > Mathboxes > bdcab | Unicode version | ||
| Description: A class defined by class abstraction using a bounded formula is bounded. (Contributed by BJ, 6-Oct-2019.) |
| Ref | Expression |
|---|---|
| bdcab.1 |
|
| Ref | Expression |
|---|---|
| bdcab |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bdcab.1 |
. . 3
| |
| 2 | 1 | bdab 15778 |
. 2
|
| 3 | 2 | bdelir 15787 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-gen 1472 ax-bd0 15753 ax-bdsb 15762 |
| This theorem depends on definitions: df-bi 117 df-clab 2192 df-bdc 15781 |
| This theorem is referenced by: bds 15791 bdcrab 15792 bdccsb 15800 bdcdif 15801 bdcun 15802 bdcin 15803 bdcpw 15809 bdcsn 15810 bdcuni 15816 bdcint 15817 bdciun 15818 bdciin 15819 bdcriota 15823 bj-bdfindis 15887 |
| Copyright terms: Public domain | W3C validator |