Theorem bdceqir 16784

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

Syntax hints:   = wceq 1402  BOUNDED wbdc 16780

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-bd0 16753

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234  df-bdc 16781

This theorem is referenced by:  bdcrab  16792  bdccsb  16800  bdcdif  16801  bdcun  16802  bdcin  16803  bdcnulALT  16806  bdcpw  16809  bdcsn  16810  bdcpr  16811  bdctp  16812  bdcuni  16816  bdcint  16817  bdciun  16818  bdciin  16819  bdcsuc  16820  bdcriota  16823