Theorem sseqtrri 3190

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 3189	1 |- A C_ C

Syntax hints:   = wceq 1353   C_ wss 3129

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 3135  df-ss 3142

This theorem is referenced by:  eqimss2i  3212  difdif2ss  3392  snsspr1  3740  snsspr2  3741  snsstp1  3742  snsstp2  3743  snsstp3  3744  prsstp12  3745  prsstp13  3746  prsstp23  3747  iunxdif2  3935  pwpwssunieq  3975  sssucid  4415  opabssxp  4700  dmresi  4962  cnvimass  4991  ssrnres  5071  cnvcnv  5081  cnvssrndm  5150  dmmpossx  6199  tfrcllemssrecs  6352  sucinc  6445  mapex  6653  exmidpw  6907  exmidpweq  6908  casefun  7083  djufun  7102  pw1ne1  7227  ressxr  8000  ltrelxr  8017  nnssnn0  9178  un0addcl  9208  un0mulcl  9209  nn0ssxnn0  9241  fzssnn  10067  fzossnn0  10174  isumclim3  11430  isprm3  12117  phimullem  12224  tgvalex  12711  eqgfval  13079  cnfldbas  13429  cnfldadd  13430  cnfldmul  13431  cnfldcj  13432  cnrest2  13706  qtopbasss  13991  tgqioo  14017