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 (B 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 A
bdceqir.maj	|- B = A

Assertion

Ref	Expression
bdceqir	|- BOUNDED B

Proof of Theorem bdceqir

Step	Hyp	Ref	Expression
1		bdceqir.min	. 2 |- BOUNDED A
2		bdceqir.maj	. . 3 |- B = A
3	2	eqcomi 2041	. 2 |- A = B
4	1, 3	bdceqi 9298	1 |- BOUNDED B

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