Theorem sseqtrrd 3975

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

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

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 3922

This theorem is referenced by:  3sstr4d  3993  fssrescdmd  7064  funfvima2d  7172  fnfvima  7173  frrlem8  8233  frrlem10  8235  fprresex  8250  oaordi  8471  omordi  8491  omlimcl  8503  oen0  8511  domunsncan  9001  f1opwfi  9265  cantnfle  9586  cantnflt  9587  cantnflem1d  9603  ttrcltr  9631  r1pwss  9699  rankxplim3  9796  acndom2  9967  fodomfi2  9973  cflm  10163  cflim2  10176  isf34lem5  10291  isf34lem7  10292  isf34lem6  10293  axdc2lem  10361  ttukeylem5  10426  wunex2  10651  ssfzunsn  13491  ccatass  14513  swrdval2  14571  splfv2a  14680  revccat  14690  cshimadifsn  14754  cshimadifsn0  14755  rtrclreclem1  14982  rtrclreclem2  14984  sumrblem  15636  prodrblem  15854  dfphi2  16703  vdwlem1  16911  basprssdmsets  17150  imasaddfnlem  17450  imasaddvallem  17451  imasvscafn  17459  imasvscaval  17460  mreexexlem4d  17571  mreexfidimd  17574  sscpwex  17740  acsmap2d  18479  gsumress  18574  subsubmgm  18602  subsubm  18708  frmdsssubm  18753  frmdss2  18755  subsubg  19046  cntzmhm2  19239  cntzcmnf  19742  ablcntzd  19754  gsumzsubmcl  19815  gsumconst  19831  gsumzmhm  19834  subgdmdprd  19933  dprdcntz2  19937  dprd2da  19941  dmdprdsplit2lem  19944  ablfac1eu  19972  pgpfaclem1  19980  pgpfaclem2  19981  subsubrng  20466  subsubrg  20501  issubdrg  20683  subdrgint  20706  lmhmlsp  20971  lspsntri  21019  lspindpi  21057  lidldvgen  21259  gsumfsum  21359  mrccss  21619  frlmsslsp  21721  opsrtoslem2  21979  ressply1evl  22273  scmatsgrp1  22425  toponss  22830  ssntr  22961  elcls3  22986  toponmre  22996  neiptoptop  23034  neiptopnei  23035  neitr  23083  ordtbas  23095  ordtopn1  23097  ordtopn2  23098  iscnp3  23147  tgcn  23155  tgcnp  23156  ssidcn  23158  cnclsi  23175  cncls  23177  cncnp  23183  lmcld  23206  tgcmp  23304  cnconn  23325  connima  23328  clsconn  23333  conncompcld  23337  1stccnp  23365  kgentopon  23441  llycmpkgen2  23453  1stckgen  23457  kgencn2  23460  ptopn  23486  txcls  23507  ptpjcn  23514  ptclsg  23518  xkoccn  23522  txcnp  23523  ptcnplem  23524  txcmplem2  23545  xkoptsub  23557  xkopt  23558  xkoco2cn  23561  xkococnlem  23562  xkoinjcn  23590  imasnopn  23593  imasncld  23594  imasncls  23595  qtopkgen  23613  basqtop  23614  tgqtop  23615  qtoprest  23620  kqsat  23634  kqcldsat  23636  kqnrmlem1  23646  kqnrmlem2  23647  hmeontr  23672  reghmph  23696  nrmhmph  23697  fmfnfmlem4  23860  fmfnfm  23861  flimopn  23878  flimclslem  23887  flfnei  23894  lmflf  23908  txflf  23909  fclsopn  23917  fclsfnflim  23930  alexsublem  23947  ptcmplem3  23957  cnextcn  23970  efmndtmd  24004  submtmd  24007  subgtgp  24008  symgtgp  24009  clssubg  24012  clsnsg  24013  tgpconncompeqg  24015  snclseqg  24019  tsmscls  24041  trust  24133  restutop  24141  restutopopn  24142  utop3cls  24155  utopreg  24156  trcfilu  24197  blssec  24339  prdsbl  24395  blssopn  24399  metcnp  24445  cfilucfil  24463  psmetutop  24471  iccntr  24726  icccmplem2  24728  reconnlem1  24731  metnrmlem1a  24763  metnrmlem1  24764  metnrmlem2  24765  metnrmlem3  24766  cnheibor  24870  lebnumlem1  24876  lebnumlem3  24878  lebnumii  24881  clsocv  25166  iscfil2  25182  iscmet3  25209  cmetss  25232  relcmpcmet  25234  bcthlem5  25244  itg1addlem5  25617  perfdvf  25820  dvres3  25830  dvres3a  25831  dvcmul  25863  dvcmulf  25864  dvlip2  25916  lhop1lem  25934  dvcnvrelem1  25938  dvcnvrelem2  25939  dvcnvre  25940  dvcvx  25941  plyco0  26113  plyaddlem1  26134  plymullem1  26135  aalioulem3  26258  ulmdvlem1  26325  precsexlem6  28137  precsexlem7  28138  bdayn0p1  28281  axcontlem10  28936  eengtrkg  28949  wlkp1lem7  29641  cyclnumvtx  29763  1wlkdlem4  30102  hsupunss  31305  pjpjpre  31381  ssmd2  32274  superpos  32316  atexch  32343  curry2ima  32665  pfxf1  32896  gsumhashmul  33027  symgcom2  33039  pmtrcnelor  33046  cycpmco2lem7  33087  cycpmconjvlem  33096  cycpmconjv  33097  cyc3conja  33112  elrgspnsubrunlem2  33198  subsdrg  33247  nsgmgc  33359  nsgqusf1olem3  33362  elrspunidl  33375  mxidlprm  33417  rprmdvdsprod  33481  dfufd2lem  33496  lssdimle  33579  dimkerim  33599  fedgmullem1  33601  fedgmullem2  33602  fedgmul  33603  dimlssid  33604  fldsdrgfldext2  33634  fldextrspunlsplem  33644  fldextrspunlsp  33645  fldextrspunlem1  33646  fldextrspundgdvdslem  33651  fldextrspundgdvds  33652  constr01  33708  constrmon  33710  constrextdg2lem  33714  constrext2chnlem  33716  madjusmdetlem2  33794  zarclsun  33836  rhmpreimacnlem  33850  ordtconnlem1  33890  measiuns  34183  imambfm  34229  cnmbfm  34230  dya2iocnrect  34248  omsfval  34261  omssubaddlem  34266  omssubadd  34267  totprobd  34393  fzssfzo  34506  signstfvn  34536  bnj999  34924  bnj1408  35002  bnj1442  35015  bnj1450  35016  bnj1501  35033  fnrelpredd  35055  revwlk  35097  cvmsss2  35246  cvmliftmolem1  35253  cvmliftlem3  35259  cvmlift2lem9  35283  cvmlift2lem11  35285  cvmlift3lem6  35296  cvmlift3lem7  35297  ssmclslem  35537  mclsax  35541  mclsppslem  35555  mclspps  35556  dfrdg2  35768  neiin  36305  neibastop2  36334  filnetlem4  36354  weiunfrlem  36437  rdgssun  37351  lindsdom  37593  poimirlem11  37610  poimirlem12  37611  itg2addnclem2  37651  cnres2  37742  sstotbnd2  37753  sstotbnd  37754  prdstotbnd  37773  heibor1lem  37788  igenval2  38045  lshpnelb  38962  lcvexchlem4  39015  lsatexch  39021  l1cvat  39033  lkrscss  39076  lkrss  39146  lkreqN  39148  paddunN  39906  osumcllem2N  39936  pmapojoinN  39947  pl42lem2N  39959  dibglbN  41145  diblss  41149  dicvaddcl  41169  dicvscacl  41170  diclss  41172  cdlemn5pre  41179  dihord5apre  41241  dihglblem3N  41274  dihglb2  41321  dochsat  41362  dochshpncl  41363  djhspss  41385  dihsumssj  41387  mapdlsm  41643  hdmaprnlem3eN  41837  hdmaplkr  41892  fnwe2lem2  43024  lnmlsslnm  43054  lmhmfgima  43057  hbtlem6  43102  omabs2  43305  tfsconcatrev  43321  naddwordnexlem0  43369  trrelsuperreldg  43641  iunrelexpuztr  43692  clsk1indlem2  44015  grumnudlem  44258  dvsconst  44303  dvsinax  45895  dvbdfbdioolem1  45910  itgsinexplem1  45936  itgperiod  45963  stoweidlem39  46021  dirkeritg  46084  fourierdlem48  46136  fourierdlem49  46137  fourierdlem70  46158  fourierdlem71  46159  fourierdlem81  46169  issalgend  46320  f1oresf1o  47275  clnbgrgrim  47919  rmsuppss  48355  restcls2lem  48898  iscnrm3rlem7  48931