Theorem bdceqir 17036

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

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

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 17005

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

This theorem is used by:  bdcrab  17044  bdccsb  17052  bdcdif  17053  bdcun  17054  bdcin  17055  bdcnulALT  17058  bdcpw  17061  bdcsn  17062  bdcpr  17063  bdctp  17064  bdcuni  17068  bdcint  17069  bdciun  17070  bdciin  17071  bdcsuc  17072  bdcriota  17075