Theorem bdceqir 9964

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

Syntax hints:   = wceq 1243  BOUNDED wbdc 9960

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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022  ax-bd0 9933

This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036  df-bdc 9961

This theorem is referenced by:  bdcrab  9972  bdccsb  9980  bdcdif  9981  bdcun  9982  bdcin  9983  bdcnulALT  9986  bdcpw  9989  bdcsn  9990  bdcpr  9991  bdctp  9992  bdcuni  9996  bdcint  9997  bdciun  9998  bdciin  9999  bdcsuc  10000  bdcriota  10003