| Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > Mathboxes > bdceqir | GIF version | ||
| Description: A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 15712) equality in the hypothesis, to work better with definitions (𝐵 is the definiendum that one wants to prove bounded; see comment of bd0r 15694). (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 2208 | . 2 ⊢ 𝐴 = 𝐵 |
| 4 | 1, 3 | bdceqi 15712 | 1 ⊢ BOUNDED 𝐵 |
| Colors of variables: wff set class |
| Syntax hints: = wceq 1372 BOUNDED wbdc 15709 |
| 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-5 1469 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-4 1532 ax-17 1548 ax-ial 1556 ax-ext 2186 ax-bd0 15682 |
| This theorem depends on definitions: df-bi 117 df-cleq 2197 df-clel 2200 df-bdc 15710 |
| This theorem is referenced by: bdcrab 15721 bdccsb 15729 bdcdif 15730 bdcun 15731 bdcin 15732 bdcnulALT 15735 bdcpw 15738 bdcsn 15739 bdcpr 15740 bdctp 15741 bdcuni 15745 bdcint 15746 bdciun 15747 bdciin 15748 bdcsuc 15749 bdcriota 15752 |
| Copyright terms: Public domain | W3C validator |