Theorem bdceqir 17092

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

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

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 17061

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

This theorem is used by:  bdcrab  17100  bdccsb  17108  bdcdif  17109  bdcun  17110  bdcin  17111  bdcnulALT  17114  bdcpw  17117  bdcsn  17118  bdcpr  17119  bdctp  17120  bdcuni  17124  bdcint  17125  bdciun  17126  bdciin  17127  bdcsuc  17128  bdcriota  17131