Theorem bdceqir 13042

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

Syntax hints:   = wceq 1331  BOUNDED wbdc 13038

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121  ax-bd0 13011

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135  df-bdc 13039

This theorem is referenced by:  bdcrab  13050  bdccsb  13058  bdcdif  13059  bdcun  13060  bdcin  13061  bdcnulALT  13064  bdcpw  13067  bdcsn  13068  bdcpr  13069  bdctp  13070  bdcuni  13074  bdcint  13075  bdciun  13076  bdciin  13077  bdcsuc  13078  bdcriota  13081