Theorem sseqtrrd 4001

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

Hypotheses

Ref	Expression
sseqtrrd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
sseqtrrd.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
sseqtrrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sseqtrrd

Step	Hyp	Ref	Expression
1		sseqtrrd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2740	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	sseqtrd 4000	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-ss 3948

This theorem is referenced by:  3sstr4d  4019  fssrescdmd  7126  funfvima2d  7234  fnfvima  7235  frrlem8  8300  frrlem10  8302  fprresex  8317  wfrlem17OLD  8347  oaordi  8566  omordi  8586  omlimcl  8598  oen0  8606  domunsncan  9094  f1opwfi  9378  cantnfle  9693  cantnflt  9694  cantnflem1d  9710  ttrcltr  9738  r1pwss  9806  rankxplim3  9903  acndom2  10076  fodomfi2  10082  cflm  10272  cflim2  10285  isf34lem5  10400  isf34lem7  10401  isf34lem6  10402  axdc2lem  10470  ttukeylem5  10535  wunex2  10760  ssfzunsn  13592  ccatass  14609  swrdval2  14667  splfv2a  14777  revccat  14787  cshimadifsn  14851  cshimadifsn0  14852  rtrclreclem1  15079  rtrclreclem2  15081  sumrblem  15730  prodrblem  15948  dfphi2  16794  vdwlem1  17002  basprssdmsets  17242  imasaddfnlem  17545  imasaddvallem  17546  imasvscafn  17554  imasvscaval  17555  mreexexlem4d  17662  mreexfidimd  17665  sscpwex  17831  acsmap2d  18570  gsumress  18665  subsubmgm  18693  subsubm  18799  frmdsssubm  18844  frmdss2  18846  subsubg  19137  cntzmhm2  19330  cntzcmnf  19832  ablcntzd  19844  gsumzsubmcl  19905  gsumconst  19921  gsumzmhm  19924  subgdmdprd  20023  dprdcntz2  20027  dprd2da  20031  dmdprdsplit2lem  20034  ablfac1eu  20062  pgpfaclem1  20070  pgpfaclem2  20071  subsubrng  20532  subsubrg  20567  issubdrg  20750  subdrgint  20773  lmhmlsp  21017  lspsntri  21065  lspindpi  21103  lidldvgen  21307  gsumfsum  21415  mrccss  21667  frlmsslsp  21771  opsrtoslem2  22029  ressply1evl  22323  scmatsgrp1  22477  toponss  22882  ssntr  23013  elcls3  23038  toponmre  23048  neiptoptop  23086  neiptopnei  23087  neitr  23135  ordtbas  23147  ordtopn1  23149  ordtopn2  23150  iscnp3  23199  tgcn  23207  tgcnp  23208  ssidcn  23210  cnclsi  23227  cncls  23229  cncnp  23235  lmcld  23258  tgcmp  23356  cnconn  23377  connima  23380  clsconn  23385  conncompcld  23389  1stccnp  23417  kgentopon  23493  llycmpkgen2  23505  1stckgen  23509  kgencn2  23512  ptopn  23538  txcls  23559  ptpjcn  23566  ptclsg  23570  xkoccn  23574  txcnp  23575  ptcnplem  23576  txcmplem2  23597  xkoptsub  23609  xkopt  23610  xkoco2cn  23613  xkococnlem  23614  xkoinjcn  23642  imasnopn  23645  imasncld  23646  imasncls  23647  qtopkgen  23665  basqtop  23666  tgqtop  23667  qtoprest  23672  kqsat  23686  kqcldsat  23688  kqnrmlem1  23698  kqnrmlem2  23699  hmeontr  23724  reghmph  23748  nrmhmph  23749  fmfnfmlem4  23912  fmfnfm  23913  flimopn  23930  flimclslem  23939  flfnei  23946  lmflf  23960  txflf  23961  fclsopn  23969  fclsfnflim  23982  alexsublem  23999  ptcmplem3  24009  cnextcn  24022  efmndtmd  24056  submtmd  24059  subgtgp  24060  symgtgp  24061  clssubg  24064  clsnsg  24065  tgpconncompeqg  24067  snclseqg  24071  tsmscls  24093  trust  24185  restutop  24193  restutopopn  24194  utop3cls  24207  utopreg  24208  trcfilu  24249  blssec  24391  prdsbl  24449  blssopn  24453  metcnp  24499  cfilucfil  24517  psmetutop  24525  iccntr  24780  icccmplem2  24782  reconnlem1  24785  metnrmlem1a  24817  metnrmlem1  24818  metnrmlem2  24819  metnrmlem3  24820  cnheibor  24924  lebnumlem1  24930  lebnumlem3  24932  lebnumii  24935  clsocv  25221  iscfil2  25237  iscmet3  25264  cmetss  25287  relcmpcmet  25289  bcthlem5  25299  itg1addlem5  25672  perfdvf  25875  dvres3  25885  dvres3a  25886  dvcmul  25918  dvcmulf  25919  dvlip2  25971  lhop1lem  25989  dvcnvrelem1  25993  dvcnvrelem2  25994  dvcnvre  25995  dvcvx  25996  plyco0  26168  plyaddlem1  26189  plymullem1  26190  aalioulem3  26313  ulmdvlem1  26380  precsexlem6  28173  precsexlem7  28174  axcontlem10  28919  eengtrkg  28932  wlkp1lem7  29626  cyclnumvtx  29749  1wlkdlem4  30088  hsupunss  31291  pjpjpre  31367  ssmd2  32260  superpos  32302  atexch  32329  curry2ima  32654  pfxf1  32871  gsumhashmul  33008  symgcom2  33048  pmtrcnelor  33055  cycpmco2lem7  33096  cycpmconjvlem  33105  cycpmconjv  33106  cyc3conja  33121  elrgspnsubrunlem2  33196  subsdrg  33245  nsgmgc  33380  nsgqusf1olem3  33383  elrspunidl  33396  mxidlprm  33438  rprmdvdsprod  33502  dfufd2lem  33517  lssdimle  33598  dimkerim  33618  fedgmullem1  33620  fedgmullem2  33621  fedgmul  33622  dimlssid  33623  fldsdrgfldext2  33655  fldextrspunlsplem  33665  fldextrspunlsp  33666  fldextrspunlem1  33667  fldextrspundgdvdslem  33672  fldextrspundgdvds  33673  constr01  33727  constrmon  33729  constrextdg2lem  33733  constrext2chnlem  33735  madjusmdetlem2  33802  zarclsun  33844  rhmpreimacnlem  33858  ordtconnlem1  33898  measiuns  34193  imambfm  34239  cnmbfm  34240  dya2iocnrect  34258  omsfval  34271  omssubaddlem  34276  omssubadd  34277  totprobd  34403  fzssfzo  34529  signstfvn  34559  bnj999  34947  bnj1408  35025  bnj1442  35038  bnj1450  35039  bnj1501  35056  fnrelpredd  35078  revwlk  35105  cvmsss2  35254  cvmliftmolem1  35261  cvmliftlem3  35267  cvmlift2lem9  35291  cvmlift2lem11  35293  cvmlift3lem6  35304  cvmlift3lem7  35305  ssmclslem  35545  mclsax  35549  mclsppslem  35563  mclspps  35564  dfrdg2  35771  neiin  36308  neibastop2  36337  filnetlem4  36357  weiunfrlem  36440  rdgssun  37354  lindsdom  37596  poimirlem11  37613  poimirlem12  37614  itg2addnclem2  37654  cnres2  37745  sstotbnd2  37756  sstotbnd  37757  prdstotbnd  37776  heibor1lem  37791  igenval2  38048  lshpnelb  38960  lcvexchlem4  39013  lsatexch  39019  l1cvat  39031  lkrscss  39074  lkrss  39144  lkreqN  39146  paddunN  39904  osumcllem2N  39934  pmapojoinN  39945  pl42lem2N  39957  dibglbN  41143  diblss  41147  dicvaddcl  41167  dicvscacl  41168  diclss  41170  cdlemn5pre  41177  dihord5apre  41239  dihglblem3N  41272  dihglb2  41319  dochsat  41360  dochshpncl  41361  djhspss  41383  dihsumssj  41385  mapdlsm  41641  hdmaprnlem3eN  41835  hdmaplkr  41890  fnwe2lem2  43041  lnmlsslnm  43071  lmhmfgima  43074  hbtlem6  43119  omabs2  43322  tfsconcatrev  43338  naddwordnexlem0  43386  trrelsuperreldg  43658  iunrelexpuztr  43709  clsk1indlem2  44032  grumnudlem  44276  dvsconst  44321  dvsinax  45900  dvbdfbdioolem1  45915  itgsinexplem1  45941  itgperiod  45968  stoweidlem39  46026  dirkeritg  46089  fourierdlem48  46141  fourierdlem49  46142  fourierdlem70  46163  fourierdlem71  46164  fourierdlem81  46174  issalgend  46325  f1oresf1o  47275  clnbgrgrim  47875  rmsuppss  48259  restcls2lem  48794  iscnrm3rlem7  48827