Theorem bdceqir 13357

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

Syntax hints:   = wceq 1332  BOUNDED wbdc 13353

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1487  ax-17 1503  ax-ial 1511  ax-ext 2136  ax-bd0 13326

This theorem depends on definitions:  df-bi 116  df-cleq 2147  df-clel 2150  df-bdc 13354

This theorem is referenced by:  bdcrab  13365  bdccsb  13373  bdcdif  13374  bdcun  13375  bdcin  13376  bdcnulALT  13379  bdcpw  13382  bdcsn  13383  bdcpr  13384  bdctp  13385  bdcuni  13389  bdcint  13390  bdciun  13391  bdciin  13392  bdcsuc  13393  bdcriota  13396