![]() |
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 9298) equality in the hypothesis, to work better
with definitions (![]() |
Ref | Expression |
---|---|
bdceqir.min |
![]() ![]() |
bdceqir.maj |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
bdceqir |
![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bdceqir.min |
. 2
![]() ![]() | |
2 | bdceqir.maj |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | eqcomi 2041 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 3 | bdceqi 9298 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 ax-ext 2019 ax-bd0 9268 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 df-clel 2033 df-bdc 9296 |
This theorem is referenced by: bdcrab 9307 bdccsb 9315 bdcdif 9316 bdcun 9317 bdcin 9318 bdcnulALT 9321 bdcpw 9324 bdcsn 9325 bdcpr 9326 bdctp 9327 bdcuni 9331 bdcint 9332 bdciun 9333 bdciin 9334 bdcsuc 9335 bdcriota 9338 |
Copyright terms: Public domain | W3C validator |