Theorem bdceqir 14823

Description: A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 14822) equality in the hypothesis, to work better with definitions ( B is the definiendum that one wants to prove bounded; see comment of bd0r 14804). (Contributed by BJ, 3-Oct-2019.)

Hypotheses

Ref	Expression
bdceqir.min	|- BOUNDED A
bdceqir.maj	|- B = A

Assertion

Ref	Expression
bdceqir	|- BOUNDED B

Proof of Theorem bdceqir

Step	Hyp	Ref	Expression
1		bdceqir.min	. 2 |- BOUNDED A
2		bdceqir.maj	. . 3 |- B = A
3	2	eqcomi 2191	. 2 |- A = B
4	1, 3	bdceqi 14822	1 |- BOUNDED B

Syntax hints:   = wceq 1363  BOUNDED wbdc 14819

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169  ax-bd0 14792

This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-clel 2183  df-bdc 14820

This theorem is referenced by:  bdcrab  14831  bdccsb  14839  bdcdif  14840  bdcun  14841  bdcin  14842  bdcnulALT  14845  bdcpw  14848  bdcsn  14849  bdcpr  14850  bdctp  14851  bdcuni  14855  bdcint  14856  bdciun  14857  bdciin  14858  bdcsuc  14859  bdcriota  14862