Theorem sseqtrri 3191

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

Syntax hints:   = wceq 1353   C_ wss 3130

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  eqimss2i  3213  difdif2ss  3393  snsspr1  3741  snsspr2  3742  snsstp1  3743  snsstp2  3744  snsstp3  3745  prsstp12  3746  prsstp13  3747  prsstp23  3748  iunxdif2  3936  pwpwssunieq  3976  sssucid  4416  opabssxp  4701  dmresi  4963  cnvimass  4992  ssrnres  5072  cnvcnv  5082  cnvssrndm  5151  dmmpossx  6200  tfrcllemssrecs  6353  sucinc  6446  mapex  6654  exmidpw  6908  exmidpweq  6909  casefun  7084  djufun  7103  pw1ne1  7228  ressxr  8001  ltrelxr  8018  nnssnn0  9179  un0addcl  9209  un0mulcl  9210  nn0ssxnn0  9242  fzssnn  10068  fzossnn0  10175  isumclim3  11431  isprm3  12118  phimullem  12225  tgvalex  12712  eqgfval  13081  cnfldbas  13462  cnfldadd  13463  cnfldmul  13464  cnfldcj  13465  cnrest2  13739  qtopbasss  14024  tgqioo  14050