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

Theorem bdceqir 10793
Description: A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 10792) equality in the hypothesis, to work better with definitions ( B is the definiendum that one wants to prove bounded; see comment of bd0r 10774). (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 2086 . 2  |-  A  =  B
41, 3bdceqi 10792 1  |- BOUNDED  B
Colors of variables: wff set class
Syntax hints:    = wceq 1285  BOUNDED wbdc 10789
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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064  ax-bd0 10762
This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078  df-bdc 10790
This theorem is referenced by:  bdcrab  10801  bdccsb  10809  bdcdif  10810  bdcun  10811  bdcin  10812  bdcnulALT  10815  bdcpw  10818  bdcsn  10819  bdcpr  10820  bdctp  10821  bdcuni  10825  bdcint  10826  bdciun  10827  bdciin  10828  bdcsuc  10829  bdcriota  10832
  Copyright terms: Public domain W3C validator