Theorem sseqtrrd 3984

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  3sstr4d  4002  fssrescdmd  7098  funfvima2d  7206  fnfvima  7207  frrlem8  8272  frrlem10  8274  fprresex  8289  oaordi  8510  omordi  8530  omlimcl  8542  oen0  8550  domunsncan  9041  f1opwfi  9307  cantnfle  9624  cantnflt  9625  cantnflem1d  9641  ttrcltr  9669  r1pwss  9737  rankxplim3  9834  acndom2  10007  fodomfi2  10013  cflm  10203  cflim2  10216  isf34lem5  10331  isf34lem7  10332  isf34lem6  10333  axdc2lem  10401  ttukeylem5  10466  wunex2  10691  ssfzunsn  13531  ccatass  14553  swrdval2  14611  splfv2a  14721  revccat  14731  cshimadifsn  14795  cshimadifsn0  14796  rtrclreclem1  15023  rtrclreclem2  15025  sumrblem  15677  prodrblem  15895  dfphi2  16744  vdwlem1  16952  basprssdmsets  17191  imasaddfnlem  17491  imasaddvallem  17492  imasvscafn  17500  imasvscaval  17501  mreexexlem4d  17608  mreexfidimd  17611  sscpwex  17777  acsmap2d  18514  gsumress  18609  subsubmgm  18637  subsubm  18743  frmdsssubm  18788  frmdss2  18790  subsubg  19081  cntzmhm2  19274  cntzcmnf  19775  ablcntzd  19787  gsumzsubmcl  19848  gsumconst  19864  gsumzmhm  19867  subgdmdprd  19966  dprdcntz2  19970  dprd2da  19974  dmdprdsplit2lem  19977  ablfac1eu  20005  pgpfaclem1  20013  pgpfaclem2  20014  subsubrng  20472  subsubrg  20507  issubdrg  20689  subdrgint  20712  lmhmlsp  20956  lspsntri  21004  lspindpi  21042  lidldvgen  21244  gsumfsum  21351  mrccss  21603  frlmsslsp  21705  opsrtoslem2  21963  ressply1evl  22257  scmatsgrp1  22409  toponss  22814  ssntr  22945  elcls3  22970  toponmre  22980  neiptoptop  23018  neiptopnei  23019  neitr  23067  ordtbas  23079  ordtopn1  23081  ordtopn2  23082  iscnp3  23131  tgcn  23139  tgcnp  23140  ssidcn  23142  cnclsi  23159  cncls  23161  cncnp  23167  lmcld  23190  tgcmp  23288  cnconn  23309  connima  23312  clsconn  23317  conncompcld  23321  1stccnp  23349  kgentopon  23425  llycmpkgen2  23437  1stckgen  23441  kgencn2  23444  ptopn  23470  txcls  23491  ptpjcn  23498  ptclsg  23502  xkoccn  23506  txcnp  23507  ptcnplem  23508  txcmplem2  23529  xkoptsub  23541  xkopt  23542  xkoco2cn  23545  xkococnlem  23546  xkoinjcn  23574  imasnopn  23577  imasncld  23578  imasncls  23579  qtopkgen  23597  basqtop  23598  tgqtop  23599  qtoprest  23604  kqsat  23618  kqcldsat  23620  kqnrmlem1  23630  kqnrmlem2  23631  hmeontr  23656  reghmph  23680  nrmhmph  23681  fmfnfmlem4  23844  fmfnfm  23845  flimopn  23862  flimclslem  23871  flfnei  23878  lmflf  23892  txflf  23893  fclsopn  23901  fclsfnflim  23914  alexsublem  23931  ptcmplem3  23941  cnextcn  23954  efmndtmd  23988  submtmd  23991  subgtgp  23992  symgtgp  23993  clssubg  23996  clsnsg  23997  tgpconncompeqg  23999  snclseqg  24003  tsmscls  24025  trust  24117  restutop  24125  restutopopn  24126  utop3cls  24139  utopreg  24140  trcfilu  24181  blssec  24323  prdsbl  24379  blssopn  24383  metcnp  24429  cfilucfil  24447  psmetutop  24455  iccntr  24710  icccmplem2  24712  reconnlem1  24715  metnrmlem1a  24747  metnrmlem1  24748  metnrmlem2  24749  metnrmlem3  24750  cnheibor  24854  lebnumlem1  24860  lebnumlem3  24862  lebnumii  24865  clsocv  25150  iscfil2  25166  iscmet3  25193  cmetss  25216  relcmpcmet  25218  bcthlem5  25228  itg1addlem5  25601  perfdvf  25804  dvres3  25814  dvres3a  25815  dvcmul  25847  dvcmulf  25848  dvlip2  25900  lhop1lem  25918  dvcnvrelem1  25922  dvcnvrelem2  25923  dvcnvre  25924  dvcvx  25925  plyco0  26097  plyaddlem1  26118  plymullem1  26119  aalioulem3  26242  ulmdvlem1  26309  precsexlem6  28114  precsexlem7  28115  bdayn0p1  28258  axcontlem10  28900  eengtrkg  28913  wlkp1lem7  29607  cyclnumvtx  29730  1wlkdlem4  30069  hsupunss  31272  pjpjpre  31348  ssmd2  32241  superpos  32283  atexch  32310  curry2ima  32632  pfxf1  32863  gsumhashmul  33001  symgcom2  33041  pmtrcnelor  33048  cycpmco2lem7  33089  cycpmconjvlem  33098  cycpmconjv  33099  cyc3conja  33114  elrgspnsubrunlem2  33199  subsdrg  33248  nsgmgc  33383  nsgqusf1olem3  33386  elrspunidl  33399  mxidlprm  33441  rprmdvdsprod  33505  dfufd2lem  33520  lssdimle  33603  dimkerim  33623  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  dimlssid  33628  fldsdrgfldext2  33658  fldextrspunlsplem  33668  fldextrspunlsp  33669  fldextrspunlem1  33670  fldextrspundgdvdslem  33675  fldextrspundgdvds  33676  constr01  33732  constrmon  33734  constrextdg2lem  33738  constrext2chnlem  33740  madjusmdetlem2  33818  zarclsun  33860  rhmpreimacnlem  33874  ordtconnlem1  33914  measiuns  34207  imambfm  34253  cnmbfm  34254  dya2iocnrect  34272  omsfval  34285  omssubaddlem  34290  omssubadd  34291  totprobd  34417  fzssfzo  34530  signstfvn  34560  bnj999  34948  bnj1408  35026  bnj1442  35039  bnj1450  35040  bnj1501  35057  fnrelpredd  35079  revwlk  35112  cvmsss2  35261  cvmliftmolem1  35268  cvmliftlem3  35274  cvmlift2lem9  35298  cvmlift2lem11  35300  cvmlift3lem6  35311  cvmlift3lem7  35312  ssmclslem  35552  mclsax  35556  mclsppslem  35570  mclspps  35571  dfrdg2  35783  neiin  36320  neibastop2  36349  filnetlem4  36369  weiunfrlem  36452  rdgssun  37366  lindsdom  37608  poimirlem11  37625  poimirlem12  37626  itg2addnclem2  37666  cnres2  37757  sstotbnd2  37768  sstotbnd  37769  prdstotbnd  37788  heibor1lem  37803  igenval2  38060  lshpnelb  38977  lcvexchlem4  39030  lsatexch  39036  l1cvat  39048  lkrscss  39091  lkrss  39161  lkreqN  39163  paddunN  39921  osumcllem2N  39951  pmapojoinN  39962  pl42lem2N  39974  dibglbN  41160  diblss  41164  dicvaddcl  41184  dicvscacl  41185  diclss  41187  cdlemn5pre  41194  dihord5apre  41256  dihglblem3N  41289  dihglb2  41336  dochsat  41377  dochshpncl  41378  djhspss  41400  dihsumssj  41402  mapdlsm  41658  hdmaprnlem3eN  41852  hdmaplkr  41907  fnwe2lem2  43040  lnmlsslnm  43070  lmhmfgima  43073  hbtlem6  43118  omabs2  43321  tfsconcatrev  43337  naddwordnexlem0  43385  trrelsuperreldg  43657  iunrelexpuztr  43708  clsk1indlem2  44031  grumnudlem  44274  dvsconst  44319  dvsinax  45911  dvbdfbdioolem1  45926  itgsinexplem1  45952  itgperiod  45979  stoweidlem39  46037  dirkeritg  46100  fourierdlem48  46152  fourierdlem49  46153  fourierdlem70  46174  fourierdlem71  46175  fourierdlem81  46185  issalgend  46336  f1oresf1o  47291  clnbgrgrim  47934  rmsuppss  48358  restcls2lem  48901  iscnrm3rlem7  48934