Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bdceqir Unicode version

Theorem bdceqir 11381
Description: A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 11380) equality in the hypothesis, to work better with definitions ( B is the definiendum that one wants to prove bounded; see comment of bd0r 11362). (Contributed by BJ, 3-Oct-2019.)
Hypotheses
Ref Expression
bdceqir.min  |- BOUNDED  A
bdceqir.maj  |-  B  =  A
Assertion
Ref Expression
bdceqir  |- BOUNDED  B

Proof of Theorem bdceqir
StepHypRef Expression
1 bdceqir.min . 2  |- BOUNDED  A
2 bdceqir.maj . . 3  |-  B  =  A
32eqcomi 2092 . 2  |-  A  =  B
41, 3bdceqi 11380 1  |- BOUNDED  B
Colors of variables: wff set class
Syntax hints:    = wceq 1289  BOUNDED wbdc 11377
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070  ax-bd0 11350
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084  df-bdc 11378
This theorem is referenced by:  bdcrab  11389  bdccsb  11397  bdcdif  11398  bdcun  11399  bdcin  11400  bdcnulALT  11403  bdcpw  11406  bdcsn  11407  bdcpr  11408  bdctp  11409  bdcuni  11413  bdcint  11414  bdciun  11415  bdciin  11416  bdcsuc  11417  bdcriota  11420
  Copyright terms: Public domain W3C validator