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

Theorem bdceqir 9299
Description: A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 9298) equality in the hypothesis, to work better with definitions ( is the definiendum that one wants to prove bounded; see comment of bd0r 9280). (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 2041 . 2
41, 3bdceqi 9298 1 BOUNDED
Colors of variables: wff set class
Syntax hints:   wceq 1242  BOUNDED wbdc 9295
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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019  ax-bd0 9268
This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-clel 2033  df-bdc 9296
This theorem is referenced by:  bdcrab  9307  bdccsb  9315  bdcdif  9316  bdcun  9317  bdcin  9318  bdcnulALT  9321  bdcpw  9324  bdcsn  9325  bdcpr  9326  bdctp  9327  bdcuni  9331  bdcint  9332  bdciun  9333  bdciin  9334  bdcsuc  9335  bdcriota  9338
  Copyright terms: Public domain W3C validator