Theorem sseqtrri 3283

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

Syntax hints:   = wceq 1402   C_ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  eqimss2i  3305  difdif2ss  3488  snsspr1  3858  snsspr2  3859  snsstp1  3860  snsstp2  3861  snsstp3  3862  prsstp12  3863  prsstp13  3864  prsstp23  3865  iunxdif2  4056  pwpwssunieq  4096  sssucid  4555  opabssxp  4844  dmresi  5113  cnvimass  5145  ssrnres  5225  cnvcnv  5235  cnvssrndm  5304  dmmpossx  6425  tfrcllemssrecs  6613  sucinc  6708  mapex  6918  exmidpw  7205  exmidpweq  7206  casefun  7415  djufun  7434  pw1ne1  7578  ressxr  8359  ltrelxr  8376  nnssnn0  9545  un0addcl  9575  un0mulcl  9576  nn0ssxnn0  9612  fzssnn  10452  fzossnn0  10562  isumclim3  12168  isprm3  12874  phimullem  12981  ballotfilem7  13257  tgvalex  13594  eqgfval  14002  cnfldbas  14869  mpocnfldadd  14870  mpocnfldmul  14872  cnfldcj  14874  cnfldtset  14875  cnfldle  14876  cnfldds  14877  cnrest2  15260  qtopbasss  15545  tgqioo  15579