Theorem bdceqir 13031

Description: A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 13030) equality in the hypothesis, to work better with definitions (𝐵 is the definiendum that one wants to prove bounded; see comment of bd0r 13012). (Contributed by BJ, 3-Oct-2019.)

Hypotheses

Ref	Expression
bdceqir.min	⊢ BOUNDED 𝐴
bdceqir.maj	⊢ 𝐵 = 𝐴

Assertion

Ref	Expression
bdceqir	⊢ BOUNDED 𝐵

Proof of Theorem bdceqir

Step	Hyp	Ref	Expression
1		bdceqir.min	. 2 ⊢ BOUNDED 𝐴
2		bdceqir.maj	. . 3 ⊢ 𝐵 = 𝐴
3	2	eqcomi 2141	. 2 ⊢ 𝐴 = 𝐵
4	1, 3	bdceqi 13030	1 ⊢ BOUNDED 𝐵

Syntax hints:   = wceq 1331  BOUNDED wbdc 13027

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 2119  ax-bd0 13000

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133  df-bdc 13028

This theorem is referenced by:  bdcrab  13039  bdccsb  13047  bdcdif  13048  bdcun  13049  bdcin  13050  bdcnulALT  13053  bdcpw  13056  bdcsn  13057  bdcpr  13058  bdctp  13059  bdcuni  13063  bdcint  13064  bdciun  13065  bdciin  13066  bdcsuc  13067  bdcriota  13070