Theorem bdceqir 11381

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

Syntax hints:   = wceq 1289  BOUNDED wbdc 11377

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 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070  ax-bd0 11350

This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084  df-bdc 11378

This theorem is referenced by:  bdcrab  11389  bdccsb  11397  bdcdif  11398  bdcun  11399  bdcin  11400  bdcnulALT  11403  bdcpw  11406  bdcsn  11407  bdcpr  11408  bdctp  11409  bdcuni  11413  bdcint  11414  bdciun  11415  bdciin  11416  bdcsuc  11417  bdcriota  11420