Theorem sseqtrrd 3973

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

Syntax hints:   → wi 4   = wceq 1559   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3921

This theorem is referenced by:  3sstr4d  3991  fssrescdmd  7104  funfvima2d  7212  fnfvima  7213  frrlem8  8269  frrlem10  8271  fprresex  8286  oaordi  8510  omordi  8530  omlimcl  8542  oen0  8551  domunsncan  9045  f1opwfi  9296  cantnfle  9623  cantnflt  9624  cantnflem1d  9640  ttrcltr  9668  r1pwss  9739  rankxplim3  9836  acndom2  10007  fodomfi2  10013  cflm  10203  cflim2  10217  isf34lem5  10332  isf34lem7  10333  isf34lem6  10334  axdc2lem  10402  ttukeylem5  10467  wunex2  10693  ssfzunsn  13572  ccatass  14599  swrdval2  14657  splfv2a  14766  revccat  14776  cshimadifsn  14839  cshimadifsn0  14840  rtrclreclem1  15067  rtrclreclem2  15069  sumrblem  15721  prodrblem  15942  dfphi2  16792  vdwlem1  17000  basprssdmsets  17240  imasaddfnlem  17541  imasaddvallem  17542  imasvscafn  17550  imasvscaval  17551  mreexexlem4d  17662  mreexfidimd  17665  sscpwex  17831  acsmap2d  18570  gsumress  18699  subsubmgm  18727  subsubm  18833  frmdsssubm  18878  frmdss2  18880  subsubg  19174  cntzmhm2  19365  cntzcmnf  19868  ablcntzd  19880  gsumzsubmcl  19941  gsumconst  19957  gsumzmhm  19960  subgdmdprd  20059  dprdcntz2  20063  dprd2da  20067  dmdprdsplit2lem  20070  ablfac1eu  20098  pgpfaclem1  20106  pgpfaclem2  20107  subsubrng  20592  subsubrg  20627  issubdrg  20809  subdrgint  20832  lmhmlsp  21096  lspsntri  21144  lspindpi  21182  lidldvgen  21384  gsumfsum  21466  mrccss  21726  frlmsslsp  21828  opsrtoslem2  22089  ressply1evl  22413  scmatsgrp1  22562  toponss  22967  ssntr  23098  elcls3  23123  toponmre  23133  neiptoptop  23171  neiptopnei  23172  neitr  23220  ordtbas  23232  ordtopn1  23234  ordtopn2  23235  iscnp3  23284  tgcn  23292  tgcnp  23293  ssidcn  23295  cnclsi  23312  cncls  23314  cncnp  23320  lmcld  23343  tgcmp  23441  cnconn  23462  connima  23465  clsconn  23470  conncompcld  23474  1stccnp  23502  kgentopon  23578  llycmpkgen2  23590  1stckgen  23594  kgencn2  23597  ptopn  23623  txcls  23644  ptpjcn  23651  ptclsg  23655  xkoccn  23659  txcnp  23660  ptcnplem  23661  txcmplem2  23682  xkoptsub  23694  xkopt  23695  xkoco2cn  23698  xkococnlem  23699  xkoinjcn  23727  imasnopn  23730  imasncld  23731  imasncls  23732  qtopkgen  23750  basqtop  23751  tgqtop  23752  qtoprest  23757  kqsat  23771  kqcldsat  23773  kqnrmlem1  23783  kqnrmlem2  23784  hmeontr  23809  reghmph  23833  nrmhmph  23834  fmfnfmlem4  23997  fmfnfm  23998  flimopn  24015  flimclslem  24024  flfnei  24031  lmflf  24045  txflf  24046  fclsopn  24054  fclsfnflim  24067  alexsublem  24084  ptcmplem3  24094  cnextcn  24107  efmndtmd  24141  submtmd  24144  subgtgp  24145  symgtgp  24146  clssubg  24149  clsnsg  24150  tgpconncompeqg  24152  snclseqg  24156  tsmscls  24178  trust  24269  restutop  24277  restutopopn  24278  utop3cls  24291  utopreg  24292  trcfilu  24333  blssec  24475  prdsbl  24531  blssopn  24535  metcnp  24581  cfilucfil  24599  psmetutop  24607  iccntr  24862  icccmplem2  24864  reconnlem1  24867  metnrmlem1a  24899  metnrmlem1  24900  metnrmlem2  24901  metnrmlem3  24902  cnheibor  24997  lebnumlem1  25003  lebnumlem3  25005  lebnumii  25008  clsocv  25292  iscfil2  25308  iscmet3  25335  cmetss  25358  relcmpcmet  25360  bcthlem5  25370  itg1addlem5  25742  perfdvf  25945  dvres3  25955  dvres3a  25956  dvcmul  25986  dvcmulf  25987  dvlip2  26037  lhop1lem  26055  dvcnvrelem1  26059  dvcnvrelem2  26060  dvcnvre  26061  dvcvx  26062  plyco0  26232  plyaddlem1  26253  plymullem1  26254  aalioulem3  26375  ulmdvlem1  26440  precsexlem6  28282  precsexlem7  28283  bdayn0p1  28439  bdaypw2n0bndlem  28533  z12bdaylem2  28541  axcontlem10  29120  eengtrkg  29133  wlkp1lem7  29824  cyclnumvtx  29946  1wlkdlem4  30288  hsupunss  31492  pjpjpre  31568  ssmd2  32461  superpos  32503  atexch  32530  curry2ima  32861  pfxf1  33081  gsumhashmul  33208  symgcom2  33225  pmtrcnelor  33232  cycpmco2lem7  33273  cycpmconjvlem  33282  cycpmconjv  33283  cyc3conja  33298  elrgspnsubrunlem2  33390  subsdrg  33446  nsgmgc  33559  nsgqusf1olem3  33562  elrspunidl  33575  mxidlprm  33619  rprmdvdsprod  33691  dfufd2lem  33706  esplyfvaln  33832  lssdimle  33866  dimkerim  33885  fedgmullem1  33887  fedgmullem2  33888  fedgmul  33889  dimlssid  33890  fldsdrgfldext2  33920  fldextrspunlsplem  33931  fldextrspunlsp  33932  fldextrspunlem1  33933  fldextrspundgdvdslem  33938  fldextrspundgdvds  33939  constr01  34000  constrmon  34002  constrextdg2lem  34006  constrext2chnlem  34008  madjusmdetlem2  34086  zarclsun  34128  rhmpreimacnlem  34142  ordtconnlem1  34182  measiuns  34475  imambfm  34520  cnmbfm  34521  dya2iocnrect  34539  omsfval  34552  omssubaddlem  34557  omssubadd  34558  totprobd  34684  fzssfzo  34797  signstfvn  34827  bnj999  35217  bnj1408  35295  bnj1442  35308  bnj1450  35309  bnj1501  35326  fnrelpredd  35351  revwlk  35439  cvmsss2  35588  cvmliftmolem1  35595  cvmliftlem3  35601  cvmlift2lem9  35625  cvmlift2lem11  35627  cvmlift3lem6  35638  cvmlift3lem7  35639  ssmclslem  35879  mclsax  35883  mclsppslem  35897  mclspps  35898  dfrdg2  36107  neiin  36656  neibastop2  36685  filnetlem4  36705  weiunfrlem  36788  rdgssun  37836  lindsdom  38077  poimirlem11  38094  poimirlem12  38095  itg2addnclem2  38135  cnres2  38226  sstotbnd2  38237  sstotbnd  38238  prdstotbnd  38257  heibor1lem  38272  igenval2  38529  lshpnelb  39572  lcvexchlem4  39625  lsatexch  39631  l1cvat  39643  lkrscss  39686  lkrss  39756  lkreqN  39758  paddunN  40515  osumcllem2N  40545  pmapojoinN  40556  pl42lem2N  40568  dibglbN  41754  diblss  41758  dicvaddcl  41778  dicvscacl  41779  diclss  41781  cdlemn5pre  41788  dihord5apre  41850  dihglblem3N  41883  dihglb2  41930  dochsat  41971  dochshpncl  41972  djhspss  41994  dihsumssj  41996  mapdlsm  42252  hdmaprnlem3eN  42446  hdmaplkr  42501  fnwe2lem2  43592  lnmlsslnm  43622  lmhmfgima  43625  hbtlem6  43670  omabs2  43873  tfsconcatrev  43889  naddwordnexlem0  43937  trrelsuperreldg  44208  iunrelexpuztr  44259  clsk1indlem2  44582  grumnudlem  44825  dvsconst  44870  dvsinax  46451  dvbdfbdioolem1  46466  itgsinexplem1  46492  itgperiod  46519  stoweidlem39  46577  dirkeritg  46640  fourierdlem48  46692  fourierdlem49  46693  fourierdlem70  46714  fourierdlem71  46715  fourierdlem81  46725  issalgend  46876  chnsubseqwl  47419  f1oresf1o  47848  clnbgrgrim  48520  rmsuppss  48956  restcls2lem  49498  iscnrm3rlem7  49531