Theorem bdceqir 13879

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

Syntax hints:   = wceq 1348  BOUNDED wbdc 13875

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-bd0 13848

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166  df-bdc 13876

This theorem is referenced by:  bdcrab  13887  bdccsb  13895  bdcdif  13896  bdcun  13897  bdcin  13898  bdcnulALT  13901  bdcpw  13904  bdcsn  13905  bdcpr  13906  bdctp  13907  bdcuni  13911  bdcint  13912  bdciun  13913  bdciin  13914  bdcsuc  13915  bdcriota  13918