Theorem sseqtrri 3232

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)

Hypotheses

Ref	Expression
sseqtrri.1	|- A C_ B
sseqtrri.2	|- C = B

Assertion

Ref	Expression
sseqtrri	|- A C_ C

Proof of Theorem sseqtrri

Step	Hyp	Ref	Expression
1		sseqtrri.1	. 2 |- A C_ B
2		sseqtrri.2	. . 3 |- C = B
3	2	eqcomi 2210	. 2 |- B = C
4	1, 3	sseqtri 3231	1 |- A C_ C

Syntax hints:   = wceq 1373   C_ wss 3170

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  eqimss2i  3254  difdif2ss  3434  snsspr1  3787  snsspr2  3788  snsstp1  3789  snsstp2  3790  snsstp3  3791  prsstp12  3792  prsstp13  3793  prsstp23  3794  iunxdif2  3982  pwpwssunieq  4022  sssucid  4470  opabssxp  4757  dmresi  5023  cnvimass  5054  ssrnres  5134  cnvcnv  5144  cnvssrndm  5213  dmmpossx  6298  tfrcllemssrecs  6451  sucinc  6544  mapex  6754  exmidpw  7020  exmidpweq  7021  casefun  7202  djufun  7221  pw1ne1  7360  ressxr  8136  ltrelxr  8153  nnssnn0  9318  un0addcl  9348  un0mulcl  9349  nn0ssxnn0  9381  fzssnn  10210  fzossnn0  10319  isumclim3  11809  isprm3  12515  phimullem  12622  tgvalex  13170  eqgfval  13633  cnfldbas  14397  mpocnfldadd  14398  mpocnfldmul  14400  cnfldcj  14402  cnfldtset  14403  cnfldle  14404  cnfldds  14405  cnrest2  14783  qtopbasss  15068  tgqioo  15102