Theorem bdceqir 13213

Description: A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 13212) equality in the hypothesis, to work better with definitions ( B is the definiendum that one wants to prove bounded; see comment of bd0r 13194). (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 2144	. 2 |- A = B
4	1, 3	bdceqi 13212	1 |- BOUNDED B

Syntax hints:   = wceq 1332  BOUNDED wbdc 13209

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122  ax-bd0 13182

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136  df-bdc 13210

This theorem is referenced by:  bdcrab  13221  bdccsb  13229  bdcdif  13230  bdcun  13231  bdcin  13232  bdcnulALT  13235  bdcpw  13238  bdcsn  13239  bdcpr  13240  bdctp  13241  bdcuni  13245  bdcint  13246  bdciun  13247  bdciin  13248  bdcsuc  13249  bdcriota  13252