Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > Mathboxes > bdceqir | Unicode version |
Description: A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 13041) equality in the hypothesis, to work better with definitions ( is the definiendum that one wants to prove bounded; see comment of bd0r 13023). (Contributed by BJ, 3-Oct-2019.) |
Ref | Expression |
---|---|
bdceqir.min | BOUNDED |
bdceqir.maj |
Ref | Expression |
---|---|
bdceqir | BOUNDED |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bdceqir.min | . 2 BOUNDED | |
2 | bdceqir.maj | . . 3 | |
3 | 2 | eqcomi 2143 | . 2 |
4 | 1, 3 | bdceqi 13041 | 1 BOUNDED |
Colors of variables: wff set class |
Syntax hints: wceq 1331 BOUNDED wbdc 13038 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 ax-ext 2121 ax-bd0 13011 |
This theorem depends on definitions: df-bi 116 df-cleq 2132 df-clel 2135 df-bdc 13039 |
This theorem is referenced by: bdcrab 13050 bdccsb 13058 bdcdif 13059 bdcun 13060 bdcin 13061 bdcnulALT 13064 bdcpw 13067 bdcsn 13068 bdcpr 13069 bdctp 13070 bdcuni 13074 bdcint 13075 bdciun 13076 bdciin 13077 bdcsuc 13078 bdcriota 13081 |
Copyright terms: Public domain | W3C validator |