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

Theorem bdceqir 13879
Description: A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 13878) equality in the hypothesis, to work better with definitions ( B is the definiendum that one wants to prove bounded; see comment of bd0r 13860). (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 2174 . 2  |-  A  =  B
41, 3bdceqi 13878 1  |- BOUNDED  B
Colors of variables: wff set class
Syntax hints:    = wceq 1348  BOUNDED wbdc 13875
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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-bd0 13848
This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166  df-bdc 13876
This theorem is referenced by:  bdcrab  13887  bdccsb  13895  bdcdif  13896  bdcun  13897  bdcin  13898  bdcnulALT  13901  bdcpw  13904  bdcsn  13905  bdcpr  13906  bdctp  13907  bdcuni  13911  bdcint  13912  bdciun  13913  bdciin  13914  bdcsuc  13915  bdcriota  13918
  Copyright terms: Public domain W3C validator