Theorem bdceqir 17075

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

This proof depends on syntax axioms:   = wceq 1402  BOUNDED wbdc 17071

This proof depends on 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 17044

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234  df-bdc 17072

This theorem is used by:  bdcrab  17083  bdccsb  17091  bdcdif  17092  bdcun  17093  bdcin  17094  bdcnulALT  17097  bdcpw  17100  bdcsn  17101  bdcpr  17102  bdctp  17103  bdcuni  17107  bdcint  17108  bdciun  17109  bdciin  17110  bdcsuc  17111  bdcriota  17114