Theorem bdceqir 10635

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

Syntax hints:   = wceq 1284  BOUNDED wbdc 10631

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063  ax-bd0 10604

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077  df-bdc 10632

This theorem is referenced by:  bdcrab  10643  bdccsb  10651  bdcdif  10652  bdcun  10653  bdcin  10654  bdcnulALT  10657  bdcpw  10660  bdcsn  10661  bdcpr  10662  bdctp  10663  bdcuni  10667  bdcint  10668  bdciun  10669  bdciin  10670  bdcsuc  10671  bdcriota  10674