Theorem bdceqir 15780

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

Syntax hints:   = wceq 1373  BOUNDED wbdc 15776

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187  ax-bd0 15749

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201  df-bdc 15777

This theorem is referenced by:  bdcrab  15788  bdccsb  15796  bdcdif  15797  bdcun  15798  bdcin  15799  bdcnulALT  15802  bdcpw  15805  bdcsn  15806  bdcpr  15807  bdctp  15808  bdcuni  15812  bdcint  15813  bdciun  15814  bdciin  15815  bdcsuc  15816  bdcriota  15819