Theorem sseqtrri 3182

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

Syntax hints:   = wceq 1348   C_ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  eqimss2i  3204  difdif2ss  3384  snsspr1  3728  snsspr2  3729  snsstp1  3730  snsstp2  3731  snsstp3  3732  prsstp12  3733  prsstp13  3734  prsstp23  3735  iunxdif2  3921  pwpwssunieq  3961  sssucid  4400  opabssxp  4685  dmresi  4946  cnvimass  4974  ssrnres  5053  cnvcnv  5063  cnvssrndm  5132  dmmpossx  6178  tfrcllemssrecs  6331  sucinc  6424  mapex  6632  exmidpw  6886  exmidpweq  6887  casefun  7062  djufun  7081  pw1ne1  7206  ressxr  7963  ltrelxr  7980  nnssnn0  9138  un0addcl  9168  un0mulcl  9169  nn0ssxnn0  9201  fzssnn  10024  fzossnn0  10131  isumclim3  11386  isprm3  12072  phimullem  12179  tgvalex  12844  cnrest2  13030  qtopbasss  13315  tgqioo  13341