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

Theorem bdceqir 12844
Description: A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 12843) equality in the hypothesis, to work better with definitions ( B is the definiendum that one wants to prove bounded; see comment of bd0r 12825). (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 2119 . 2  |-  A  =  B
41, 3bdceqi 12843 1  |- BOUNDED  B
Colors of variables: wff set class
Syntax hints:    = wceq 1314  BOUNDED wbdc 12840
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097  ax-bd0 12813
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111  df-bdc 12841
This theorem is referenced by:  bdcrab  12852  bdccsb  12860  bdcdif  12861  bdcun  12862  bdcin  12863  bdcnulALT  12866  bdcpw  12869  bdcsn  12870  bdcpr  12871  bdctp  12872  bdcuni  12876  bdcint  12877  bdciun  12878  bdciin  12879  bdcsuc  12880  bdcriota  12883
  Copyright terms: Public domain W3C validator