Theorem sseqtrri 3262

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 2235	. 2 |- B = C
4	1, 3	sseqtri 3261	1 |- A C_ C

Syntax hints:   = wceq 1397   C_ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  eqimss2i  3284  difdif2ss  3464  snsspr1  3821  snsspr2  3822  snsstp1  3823  snsstp2  3824  snsstp3  3825  prsstp12  3826  prsstp13  3827  prsstp23  3828  iunxdif2  4019  pwpwssunieq  4059  sssucid  4512  opabssxp  4800  dmresi  5068  cnvimass  5099  ssrnres  5179  cnvcnv  5189  cnvssrndm  5258  dmmpossx  6363  tfrcllemssrecs  6517  sucinc  6612  mapex  6822  exmidpw  7099  exmidpweq  7100  casefun  7283  djufun  7302  pw1ne1  7446  ressxr  8222  ltrelxr  8239  nnssnn0  9404  un0addcl  9434  un0mulcl  9435  nn0ssxnn0  9467  fzssnn  10302  fzossnn0  10411  isumclim3  11983  isprm3  12689  phimullem  12796  tgvalex  13345  eqgfval  13808  cnfldbas  14573  mpocnfldadd  14574  mpocnfldmul  14576  cnfldcj  14578  cnfldtset  14579  cnfldle  14580  cnfldds  14581  cnrest2  14959  qtopbasss  15244  tgqioo  15278