Theorem sseqtrri 3962

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)

Hypotheses

Ref	Expression
sseqtrri.1	⊢ 𝐴 ⊆ 𝐵
sseqtrri.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
sseqtrri	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem sseqtrri

Step	Hyp	Ref	Expression
1		sseqtrri.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		sseqtrri.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2748	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	sseqtri 3961	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1541   ⊆ wss 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908

This theorem is referenced by:  eqimss2i  3984  difsssymdif  4191  snsspr1  4752  snsspr2  4753  snsstp1  4754  snsstp2  4755  snsstp3  4756  unissint  4908  iunxdif2  4987  pwpwssunieq  5037  intabs  5269  inxpssres  5605  opabssxp  5677  dmresi  5958  cnvimass  5986  sofld  6087  cnvcnv  6092  cnvssrndm  6171  sssucid  6340  cnvimainrn  6938  fvclss  7109  dmmpossx  7892  suppun  7984  frrlem12  8097  wfrlem14OLD  8137  tfrlem11  8203  oawordeulem  8361  mapex  8595  trcl  9469  djuunxp  9663  dfac3  9861  cfsuc  9997  isfin4p1  10055  fin23lem11  10057  domtriomlem  10182  ttukeylem1  10249  ttukeylem7  10255  brdom7disj  10271  brdom6disj  10272  fingch  10363  fpwwe2lem12  10382  canthp1lem2  10393  wunex2  10478  wunex3  10481  ressxr  11003  ltrelxr  11020  nnssnn0  12219  un0addcl  12249  un0mulcl  12250  nn0ssxnn0  12291  caubnd  15051  isumclim3  15452  iprodclim3  15691  bpoly4  15750  fprodefsum  15785  znnen  15902  isprm3  16369  phimullem  16461  isstruct2  16831  2strbas  16916  2strop  16917  2strbas1  16920  rngbase  16990  rngplusg  16991  rngmulr  16992  srngbase  17001  srngplusg  17002  srngmulr  17003  srnginvl  17004  lmodbase  17017  lmodplusg  17018  lmodsca  17019  lmodvsca  17020  ipsbase  17028  ipsaddg  17029  ipsmulr  17030  ipssca  17031  ipsvsca  17032  ipsip  17033  phlbase  17038  phlplusg  17039  phlsca  17040  phlvsca  17041  phlip  17042  topgrpbas  17053  topgrpplusg  17054  topgrptset  17055  otpsbas  17068  otpstset  17069  otpsle  17070  odrngbas  17095  odrngplusg  17096  odrngmulr  17097  odrngtset  17098  odrngle  17099  odrngds  17100  homarw  17742  ipoval  18229  ipolerval  18231  eqgfval  18785  cycsubg  18808  symgbas  18959  symgsubmefmndALT  18992  islbs3  20398  cnfldbas  20582  cnfldadd  20583  cnfldmul  20584  cnfldcj  20585  cnfldtset  20586  cnfldle  20587  cnfldds  20588  cnfldunif  20589  basdif0  22084  iscldtop  22227  iocpnfordt  22347  icomnfordt  22348  iooordt  22349  cnrest2  22418  cmpcov2  22522  fiuncmp  22536  bwth  22542  indisconn  22550  locfincmp  22658  xkococnlem  22791  hmphdis  22928  uzrest  23029  ufildr  23063  fin1aufil  23064  eltsms  23265  ustval  23335  qtopbaslem  23903  tgqioo  23944  re2ndc  23945  xrhmeo  24090  bndth  24102  pi1xfrcnvlem  24200  ovolficcss  24614  nulmbl2  24681  uniiccdif  24723  opnmbllem  24746  opnmblALT  24748  mbfimaopnlem  24800  i1fima  24823  i1fima2  24824  i1fd  24826  c1liplem1  25141  deg1n0ima  25235  efcvx  25589  dvrelog  25773  dvloglem  25784  logf1o2  25786  dvlog  25787  ressatans  26065  wilthlem3  26200  trkgbas  26787  trkgdist  26788  trkgitv  26789  ex-ss  28770  ajfval  29150  ipasslem8  29178  hlimcaui  29577  shsspwh  29587  hhssabloi  29603  hhssnv  29605  hhshsslem1  29608  shunssji  29710  sshhococi  29887  pjoml6i  29930  osumcori  29984  mayete3i  30069  mayetes3i  30070  imaelshi  30399  pjclem1  30536  pjci  30541  mdcompli  30770  dmdcompli  30771  xppreima  30962  gsummpt2co  31287  cycpmrn  31389  circtopn  31766  esumpcvgval  32025  esumcvg  32033  ldgenpisyslem3  32112  elmbfmvol2  32213  sxbrsigalem0  32217  eulerpartlemsv3  32307  ballotlem7  32481  rpsqrtcn  32552  bnj931  32729  bnj1137  32954  subfacp1lem2a  33121  subfacp1lem2b  33122  erdszelem2  33133  kur14lem7  33153  kur14lem9  33155  dfon2lem2  33739  bday1s  34004  bj-snglsstag  35150  bj-2upln1upl  35193  bj-0int  35251  bj-opabssvv  35300  bj-ccssccbar  35367  bj-ccinftyssccbar  35368  bj-rvecsscvec  35454  icoreelrn  35511  finxpreclem3  35543  imadifss  35731  poimirlem4  35760  poimirlem26  35782  poimirlem27  35783  opnmbllem0  35792  mblfinlem3  35795  mblfinlem4  35796  ismblfin  35797  volsupnfl  35801  sdclem2  35879  heibor1lem  35946  refrelsredund4  36724  dicval  39169  dvhdimlem  39437  ismrc  40503  mapfzcons1cl  40520  2rexfrabdioph  40598  3rexfrabdioph  40599  4rexfrabdioph  40600  6rexfrabdioph  40601  7rexfrabdioph  40602  rabdiophlem2  40604  jm2.27dlem5  40815  algbase  40983  algaddg  40984  algmulr  40985  algsca  40986  algvsca  40987  intimass2  41216  comptiunov2i  41267  relexp0a  41277  lhe4.4ex1a  41900  iocnct  43032  iccnct  43033  dvcosre  43407  fourierdlem46  43647  fourierdlem57  43658  fourierdlem58  43659  fourierdlem62  43663  fourierdlem102  43703  fourierdlem103  43704  fourierdlem104  43705  fourierdlem114  43715  sge0split  43901  sge0uzfsumgt  43936  hoiprodp1  44080  hoidmvlelem1  44087  hoidmvlelem2  44088  hoidmvlelem3  44089  sbgoldbo  45191  dmmpossx2  45624  ipoglb0  46232  mreclat  46235  aacllem  46457