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

Theorem bdceqir 9964
Description: A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 9963) equality in the hypothesis, to work better with definitions ( B is the definiendum that one wants to prove bounded; see comment of bd0r 9945). (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 2044 . 2  |-  A  =  B
41, 3bdceqi 9963 1  |- BOUNDED  B
Colors of variables: wff set class
Syntax hints:    = wceq 1243  BOUNDED wbdc 9960
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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022  ax-bd0 9933
This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036  df-bdc 9961
This theorem is referenced by:  bdcrab  9972  bdccsb  9980  bdcdif  9981  bdcun  9982  bdcin  9983  bdcnulALT  9986  bdcpw  9989  bdcsn  9990  bdcpr  9991  bdctp  9992  bdcuni  9996  bdcint  9997  bdciun  9998  bdciin  9999  bdcsuc  10000  bdcriota  10003
  Copyright terms: Public domain W3C validator