Theorem bdceqir 16870

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

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

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 16839

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

This theorem is used by:  bdcrab  16878  bdccsb  16886  bdcdif  16887  bdcun  16888  bdcin  16889  bdcnulALT  16892  bdcpw  16895  bdcsn  16896  bdcpr  16897  bdctp  16898  bdcuni  16902  bdcint  16903  bdciun  16904  bdciin  16905  bdcsuc  16906  bdcriota  16909