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

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

Proof of Theorem bdceqir
StepHypRef Expression
1 bdceqir.min . 2 BOUNDED 𝐴
2 bdceqir.maj . . 3 𝐵 = 𝐴
32eqcomi 2087 . 2 𝐴 = 𝐵
41, 3bdceqi 11077 1 BOUNDED 𝐵
Colors of variables: wff set class
Syntax hints:   = wceq 1285  BOUNDED wbdc 11074
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 2065  ax-bd0 11047
This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-clel 2079  df-bdc 11075
This theorem is referenced by:  bdcrab  11086  bdccsb  11094  bdcdif  11095  bdcun  11096  bdcin  11097  bdcnulALT  11100  bdcpw  11103  bdcsn  11104  bdcpr  11105  bdctp  11106  bdcuni  11110  bdcint  11111  bdciun  11112  bdciin  11113  bdcsuc  11114  bdcriota  11117
  Copyright terms: Public domain W3C validator