Theorem bdceqir 10793

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

Syntax hints:   = wceq 1285  BOUNDED wbdc 10789

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 2064  ax-bd0 10762

This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078  df-bdc 10790

This theorem is referenced by:  bdcrab  10801  bdccsb  10809  bdcdif  10810  bdcun  10811  bdcin  10812  bdcnulALT  10815  bdcpw  10818  bdcsn  10819  bdcpr  10820  bdctp  10821  bdcuni  10825  bdcint  10826  bdciun  10827  bdciin  10828  bdcsuc  10829  bdcriota  10832