Theorem bdceqir 16968

Description: A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 16967) equality in the hypothesis, to work better with definitions ( B is the definiendum that one wants to prove bounded; see comment of bd0r 16949). (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 2242	. 2 |- A = B
4	1, 3	bdceqi 16967	1 |- BOUNDED B

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

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 16937

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

This theorem is used by:  bdcrab  16976  bdccsb  16984  bdcdif  16985  bdcun  16986  bdcin  16987  bdcnulALT  16990  bdcpw  16993  bdcsn  16994  bdcpr  16995  bdctp  16996  bdcuni  17000  bdcint  17001  bdciun  17002  bdciin  17003  bdcsuc  17004  bdcriota  17007