Theorem bdceqir 14635

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

Syntax hints:   = wceq 1353  BOUNDED wbdc 14631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-bd0 14604

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-bdc 14632

This theorem is referenced by:  bdcrab  14643  bdccsb  14651  bdcdif  14652  bdcun  14653  bdcin  14654  bdcnulALT  14657  bdcpw  14660  bdcsn  14661  bdcpr  14662  bdctp  14663  bdcuni  14667  bdcint  14668  bdciun  14669  bdciin  14670  bdcsuc  14671  bdcriota  14674