Theorem sseqtrrd 4036

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 4035	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

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

This theorem is referenced by:  fssrescdmd  7145  funfvima2d  7251  fnfvima  7252  frrlem8  8316  frrlem10  8318  fprresex  8333  wfrlem17OLD  8363  oaordi  8582  omordi  8602  omlimcl  8614  oen0  8622  domunsncan  9110  f1opwfi  9393  cantnfle  9708  cantnflt  9709  cantnflem1d  9725  ttrcltr  9753  r1pwss  9821  rankxplim3  9918  acndom2  10091  fodomfi2  10097  cflm  10287  cflim2  10300  isf34lem5  10415  isf34lem7  10416  isf34lem6  10417  axdc2lem  10485  ttukeylem5  10550  wunex2  10775  ssfzunsn  13606  ccatass  14622  swrdval2  14680  splfv2a  14790  revccat  14800  cshimadifsn  14864  cshimadifsn0  14865  rtrclreclem1  15092  rtrclreclem2  15094  sumrblem  15743  prodrblem  15961  dfphi2  16807  vdwlem1  17014  basprssdmsets  17257  imasaddfnlem  17574  imasaddvallem  17575  imasvscafn  17583  imasvscaval  17584  mreexexlem4d  17691  mreexfidimd  17694  sscpwex  17862  acsmap2d  18612  gsumress  18707  subsubmgm  18735  subsubm  18841  frmdsssubm  18886  frmdss2  18888  subsubg  19179  cntzmhm2  19372  cntzcmnf  19877  ablcntzd  19889  gsumzsubmcl  19950  gsumconst  19966  gsumzmhm  19969  subgdmdprd  20068  dprdcntz2  20072  dprd2da  20076  dmdprdsplit2lem  20079  ablfac1eu  20107  pgpfaclem1  20115  pgpfaclem2  20116  subsubrng  20579  subsubrg  20614  issubdrg  20797  subdrgint  20820  lmhmlsp  21065  lspsntri  21113  lspindpi  21151  lidldvgen  21361  gsumfsum  21469  mrccss  21729  frlmsslsp  21833  opsrtoslem2  22097  ressply1evl  22389  scmatsgrp1  22543  toponss  22948  ssntr  23081  elcls3  23106  toponmre  23116  neiptoptop  23154  neiptopnei  23155  neitr  23203  ordtbas  23215  ordtopn1  23217  ordtopn2  23218  iscnp3  23267  tgcn  23275  tgcnp  23276  ssidcn  23278  cnclsi  23295  cncls  23297  cncnp  23303  lmcld  23326  tgcmp  23424  cnconn  23445  connima  23448  clsconn  23453  conncompcld  23457  1stccnp  23485  kgentopon  23561  llycmpkgen2  23573  1stckgen  23577  kgencn2  23580  ptopn  23606  txcls  23627  ptpjcn  23634  ptclsg  23638  xkoccn  23642  txcnp  23643  ptcnplem  23644  txcmplem2  23665  xkoptsub  23677  xkopt  23678  xkoco2cn  23681  xkococnlem  23682  xkoinjcn  23710  imasnopn  23713  imasncld  23714  imasncls  23715  qtopkgen  23733  basqtop  23734  tgqtop  23735  qtoprest  23740  kqsat  23754  kqcldsat  23756  kqnrmlem1  23766  kqnrmlem2  23767  hmeontr  23792  reghmph  23816  nrmhmph  23817  fmfnfmlem4  23980  fmfnfm  23981  flimopn  23998  flimclslem  24007  flfnei  24014  lmflf  24028  txflf  24029  fclsopn  24037  fclsfnflim  24050  alexsublem  24067  ptcmplem3  24077  cnextcn  24090  efmndtmd  24124  submtmd  24127  subgtgp  24128  symgtgp  24129  clssubg  24132  clsnsg  24133  tgpconncompeqg  24135  snclseqg  24139  tsmscls  24161  trust  24253  restutop  24261  restutopopn  24262  utop3cls  24275  utopreg  24276  trcfilu  24318  blssec  24460  prdsbl  24519  blssopn  24523  metcnp  24569  cfilucfil  24587  psmetutop  24595  iccntr  24856  icccmplem2  24858  reconnlem1  24861  metnrmlem1a  24893  metnrmlem1  24894  metnrmlem2  24895  metnrmlem3  24896  cnheibor  25000  lebnumlem1  25006  lebnumlem3  25008  lebnumii  25011  clsocv  25297  iscfil2  25313  iscmet3  25340  cmetss  25363  relcmpcmet  25365  bcthlem5  25375  itg1addlem5  25749  perfdvf  25952  dvres3  25962  dvres3a  25963  dvcmul  25995  dvcmulf  25996  dvlip2  26048  lhop1lem  26066  dvcnvrelem1  26070  dvcnvrelem2  26071  dvcnvre  26072  dvcvx  26073  plyco0  26245  plyaddlem1  26266  plymullem1  26267  aalioulem3  26390  ulmdvlem1  26457  precsexlem6  28250  precsexlem7  28251  axcontlem10  29002  eengtrkg  29015  wlkp1lem7  29711  1wlkdlem4  30168  hsupunss  31371  pjpjpre  31447  ssmd2  32340  superpos  32382  atexch  32409  curry2ima  32723  pfxf1  32910  gsumhashmul  33046  symgcom2  33086  pmtrcnelor  33093  cycpmco2lem7  33134  cycpmconjvlem  33143  cycpmconjv  33144  cyc3conja  33159  nsgmgc  33419  nsgqusf1olem3  33422  elrspunidl  33435  mxidlprm  33477  rprmdvdsprod  33541  dfufd2lem  33556  lssdimle  33634  dimkerim  33654  fedgmullem1  33656  fedgmullem2  33657  fedgmul  33658  dimlssid  33659  constr01  33746  constrmon  33748  madjusmdetlem2  33788  zarclsun  33830  rhmpreimacnlem  33844  ordtconnlem1  33884  measiuns  34197  imambfm  34243  cnmbfm  34244  dya2iocnrect  34262  omsfval  34275  omssubaddlem  34280  omssubadd  34281  totprobd  34407  fzssfzo  34532  signstfvn  34562  bnj999  34950  bnj1408  35028  bnj1442  35041  bnj1450  35042  bnj1501  35059  fnrelpredd  35081  revwlk  35108  cvmsss2  35258  cvmliftmolem1  35265  cvmliftlem3  35271  cvmlift2lem9  35295  cvmlift2lem11  35297  cvmlift3lem6  35308  cvmlift3lem7  35309  ssmclslem  35549  mclsax  35553  mclsppslem  35567  mclspps  35568  dfrdg2  35776  neiin  36314  neibastop2  36343  filnetlem4  36363  weiunfrlem  36446  rdgssun  37360  lindsdom  37600  poimirlem11  37617  poimirlem12  37618  itg2addnclem2  37658  cnres2  37749  sstotbnd2  37760  sstotbnd  37761  prdstotbnd  37780  heibor1lem  37795  igenval2  38052  lshpnelb  38965  lcvexchlem4  39018  lsatexch  39024  l1cvat  39036  lkrscss  39079  lkrss  39149  lkreqN  39151  paddunN  39909  osumcllem2N  39939  pmapojoinN  39950  pl42lem2N  39962  dibglbN  41148  diblss  41152  dicvaddcl  41172  dicvscacl  41173  diclss  41175  cdlemn5pre  41182  dihord5apre  41244  dihglblem3N  41277  dihglb2  41324  dochsat  41365  dochshpncl  41366  djhspss  41388  dihsumssj  41390  mapdlsm  41646  hdmaprnlem3eN  41840  hdmaplkr  41895  fnwe2lem2  43039  lnmlsslnm  43069  lmhmfgima  43072  hbtlem6  43117  omabs2  43321  tfsconcatrev  43337  naddwordnexlem0  43385  trrelsuperreldg  43657  iunrelexpuztr  43708  clsk1indlem2  44031  grumnudlem  44280  dvsconst  44325  dvsinax  45868  dvbdfbdioolem1  45883  itgsinexplem1  45909  itgperiod  45936  stoweidlem39  45994  dirkeritg  46057  fourierdlem48  46109  fourierdlem49  46110  fourierdlem70  46131  fourierdlem71  46132  fourierdlem81  46142  issalgend  46293  f1oresf1o  47239  clnbgrgrim  47839  rmsuppss  48214  restcls2lem  48708  iscnrm3rlem7  48742