Theorem sseqtrrd 3960

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 2743	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	sseqtrd 3959	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  3sstr4d  3978  fssrescdmd  7073  funfvima2d  7180  fnfvima  7181  frrlem8  8236  frrlem10  8238  fprresex  8253  oaordi  8474  omordi  8494  omlimcl  8506  oen0  8515  domunsncan  9008  f1opwfi  9259  cantnfle  9583  cantnflt  9584  cantnflem1d  9600  ttrcltr  9628  r1pwss  9699  rankxplim3  9796  acndom2  9967  fodomfi2  9973  cflm  10163  cflim2  10176  isf34lem5  10291  isf34lem7  10292  isf34lem6  10293  axdc2lem  10361  ttukeylem5  10426  wunex2  10652  ssfzunsn  13515  ccatass  14542  swrdval2  14600  splfv2a  14709  revccat  14719  cshimadifsn  14782  cshimadifsn0  14783  rtrclreclem1  15010  rtrclreclem2  15012  sumrblem  15664  prodrblem  15885  dfphi2  16735  vdwlem1  16943  basprssdmsets  17182  imasaddfnlem  17483  imasaddvallem  17484  imasvscafn  17492  imasvscaval  17493  mreexexlem4d  17604  mreexfidimd  17607  sscpwex  17773  acsmap2d  18512  gsumress  18641  subsubmgm  18669  subsubm  18775  frmdsssubm  18820  frmdss2  18822  subsubg  19116  cntzmhm2  19308  cntzcmnf  19811  ablcntzd  19823  gsumzsubmcl  19884  gsumconst  19900  gsumzmhm  19903  subgdmdprd  20002  dprdcntz2  20006  dprd2da  20010  dmdprdsplit2lem  20013  ablfac1eu  20041  pgpfaclem1  20049  pgpfaclem2  20050  subsubrng  20531  subsubrg  20566  issubdrg  20748  subdrgint  20771  lmhmlsp  21036  lspsntri  21084  lspindpi  21122  lidldvgen  21324  gsumfsum  21424  mrccss  21684  frlmsslsp  21786  opsrtoslem2  22044  ressply1evl  22345  scmatsgrp1  22497  toponss  22902  ssntr  23033  elcls3  23058  toponmre  23068  neiptoptop  23106  neiptopnei  23107  neitr  23155  ordtbas  23167  ordtopn1  23169  ordtopn2  23170  iscnp3  23219  tgcn  23227  tgcnp  23228  ssidcn  23230  cnclsi  23247  cncls  23249  cncnp  23255  lmcld  23278  tgcmp  23376  cnconn  23397  connima  23400  clsconn  23405  conncompcld  23409  1stccnp  23437  kgentopon  23513  llycmpkgen2  23525  1stckgen  23529  kgencn2  23532  ptopn  23558  txcls  23579  ptpjcn  23586  ptclsg  23590  xkoccn  23594  txcnp  23595  ptcnplem  23596  txcmplem2  23617  xkoptsub  23629  xkopt  23630  xkoco2cn  23633  xkococnlem  23634  xkoinjcn  23662  imasnopn  23665  imasncld  23666  imasncls  23667  qtopkgen  23685  basqtop  23686  tgqtop  23687  qtoprest  23692  kqsat  23706  kqcldsat  23708  kqnrmlem1  23718  kqnrmlem2  23719  hmeontr  23744  reghmph  23768  nrmhmph  23769  fmfnfmlem4  23932  fmfnfm  23933  flimopn  23950  flimclslem  23959  flfnei  23966  lmflf  23980  txflf  23981  fclsopn  23989  fclsfnflim  24002  alexsublem  24019  ptcmplem3  24029  cnextcn  24042  efmndtmd  24076  submtmd  24079  subgtgp  24080  symgtgp  24081  clssubg  24084  clsnsg  24085  tgpconncompeqg  24087  snclseqg  24091  tsmscls  24113  trust  24204  restutop  24212  restutopopn  24213  utop3cls  24226  utopreg  24227  trcfilu  24268  blssec  24410  prdsbl  24466  blssopn  24470  metcnp  24516  cfilucfil  24534  psmetutop  24542  iccntr  24797  icccmplem2  24799  reconnlem1  24802  metnrmlem1a  24834  metnrmlem1  24835  metnrmlem2  24836  metnrmlem3  24837  cnheibor  24932  lebnumlem1  24938  lebnumlem3  24940  lebnumii  24943  clsocv  25227  iscfil2  25243  iscmet3  25270  cmetss  25293  relcmpcmet  25295  bcthlem5  25305  itg1addlem5  25677  perfdvf  25880  dvres3  25890  dvres3a  25891  dvcmul  25921  dvcmulf  25922  dvlip2  25972  lhop1lem  25990  dvcnvrelem1  25994  dvcnvrelem2  25995  dvcnvre  25996  dvcvx  25997  plyco0  26167  plyaddlem1  26188  plymullem1  26189  aalioulem3  26311  ulmdvlem1  26378  precsexlem6  28218  precsexlem7  28219  bdayn0p1  28375  bdaypw2n0bndlem  28469  z12bdaylem2  28477  axcontlem10  29056  eengtrkg  29069  wlkp1lem7  29761  cyclnumvtx  29883  1wlkdlem4  30225  hsupunss  31429  pjpjpre  31505  ssmd2  32398  superpos  32440  atexch  32467  curry2ima  32797  pfxf1  33017  gsumhashmul  33143  symgcom2  33160  pmtrcnelor  33167  cycpmco2lem7  33208  cycpmconjvlem  33217  cycpmconjv  33218  cyc3conja  33233  elrgspnsubrunlem2  33324  subsdrg  33374  nsgmgc  33487  nsgqusf1olem3  33490  elrspunidl  33503  mxidlprm  33545  rprmdvdsprod  33609  dfufd2lem  33624  esplyfvaln  33733  lssdimle  33767  dimkerim  33787  fedgmullem1  33789  fedgmullem2  33790  fedgmul  33791  dimlssid  33792  fldsdrgfldext2  33822  fldextrspunlsplem  33833  fldextrspunlsp  33834  fldextrspunlem1  33835  fldextrspundgdvdslem  33840  fldextrspundgdvds  33841  constr01  33902  constrmon  33904  constrextdg2lem  33908  constrext2chnlem  33910  madjusmdetlem2  33988  zarclsun  34030  rhmpreimacnlem  34044  ordtconnlem1  34084  measiuns  34377  imambfm  34422  cnmbfm  34423  dya2iocnrect  34441  omsfval  34454  omssubaddlem  34459  omssubadd  34460  totprobd  34586  fzssfzo  34699  signstfvn  34729  bnj999  35116  bnj1408  35194  bnj1442  35207  bnj1450  35208  bnj1501  35225  fnrelpredd  35250  revwlk  35323  cvmsss2  35472  cvmliftmolem1  35479  cvmliftlem3  35485  cvmlift2lem9  35509  cvmlift2lem11  35511  cvmlift3lem6  35522  cvmlift3lem7  35523  ssmclslem  35763  mclsax  35767  mclsppslem  35781  mclspps  35782  dfrdg2  35991  neiin  36530  neibastop2  36559  filnetlem4  36579  weiunfrlem  36662  rdgssun  37708  lindsdom  37949  poimirlem11  37966  poimirlem12  37967  itg2addnclem2  38007  cnres2  38098  sstotbnd2  38109  sstotbnd  38110  prdstotbnd  38129  heibor1lem  38144  igenval2  38401  lshpnelb  39444  lcvexchlem4  39497  lsatexch  39503  l1cvat  39515  lkrscss  39558  lkrss  39628  lkreqN  39630  paddunN  40387  osumcllem2N  40417  pmapojoinN  40428  pl42lem2N  40440  dibglbN  41626  diblss  41630  dicvaddcl  41650  dicvscacl  41651  diclss  41653  cdlemn5pre  41660  dihord5apre  41722  dihglblem3N  41755  dihglb2  41802  dochsat  41843  dochshpncl  41844  djhspss  41866  dihsumssj  41868  mapdlsm  42124  hdmaprnlem3eN  42318  hdmaplkr  42373  fnwe2lem2  43497  lnmlsslnm  43527  lmhmfgima  43530  hbtlem6  43575  omabs2  43778  tfsconcatrev  43794  naddwordnexlem0  43842  trrelsuperreldg  44113  iunrelexpuztr  44164  clsk1indlem2  44487  grumnudlem  44730  dvsconst  44775  dvsinax  46359  dvbdfbdioolem1  46374  itgsinexplem1  46400  itgperiod  46427  stoweidlem39  46485  dirkeritg  46548  fourierdlem48  46600  fourierdlem49  46601  fourierdlem70  46622  fourierdlem71  46623  fourierdlem81  46633  issalgend  46784  chnsubseqwl  47325  f1oresf1o  47750  clnbgrgrim  48422  rmsuppss  48858  restcls2lem  49400  iscnrm3rlem7  49433