Theorem sseqtrrd 3958

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  sseqtrrid  3970  funfvima2d  7090  fnfvima  7091  frrlem8  8080  frrlem10  8082  fprresex  8097  wfrlem17OLD  8127  oaordi  8339  omordi  8359  omlimcl  8371  oen0  8379  domunsncan  8812  f1opwfi  9053  cantnfle  9359  cantnflt  9360  cantnflem1d  9376  trpredtr  9408  r1pwss  9473  rankxplim3  9570  acndom2  9741  fodomfi2  9747  cflm  9937  cflim2  9950  isf34lem5  10065  isf34lem7  10066  isf34lem6  10067  axdc2lem  10135  ttukeylem5  10200  wunex2  10425  ssfzunsn  13231  ccatass  14221  swrdval2  14287  splfv2a  14397  revccat  14407  cshimadifsn  14470  cshimadifsn0  14471  rtrclreclem1  14696  rtrclreclem2  14698  sumrblem  15351  prodrblem  15567  dfphi2  16403  vdwlem1  16610  basprssdmsets  16853  imasaddfnlem  17156  imasaddvallem  17157  imasvscafn  17165  imasvscaval  17166  mreexexlem4d  17273  mreexfidimd  17276  sscpwex  17444  acsmap2d  18188  gsumress  18281  subsubm  18370  frmdsssubm  18415  frmdss2  18417  subsubg  18693  cntzmhm2  18861  cntzcmnf  19361  ablcntzd  19373  gsumzsubmcl  19434  gsumconst  19450  gsumzmhm  19453  subgdmdprd  19552  dprdcntz2  19556  dprd2da  19560  dmdprdsplit2lem  19563  ablfac1eu  19591  pgpfaclem1  19599  pgpfaclem2  19600  issubdrg  19964  subsubrg  19965  subdrgint  19986  lmhmlsp  20226  lspsntri  20274  lspindpi  20309  lidldvgen  20439  gsumfsum  20577  mrccss  20811  frlmsslsp  20913  opsrtoslem2  21173  scmatsgrp1  21579  toponss  21984  ssntr  22117  elcls3  22142  toponmre  22152  neiptoptop  22190  neiptopnei  22191  neitr  22239  ordtbas  22251  ordtopn1  22253  ordtopn2  22254  iscnp3  22303  tgcn  22311  tgcnp  22312  ssidcn  22314  cnclsi  22331  cncls  22333  cncnp  22339  lmcld  22362  tgcmp  22460  cnconn  22481  connima  22484  clsconn  22489  conncompcld  22493  1stccnp  22521  kgentopon  22597  llycmpkgen2  22609  1stckgen  22613  kgencn2  22616  ptopn  22642  txcls  22663  ptpjcn  22670  ptclsg  22674  xkoccn  22678  txcnp  22679  ptcnplem  22680  txcmplem2  22701  xkoptsub  22713  xkopt  22714  xkoco2cn  22717  xkococnlem  22718  xkoinjcn  22746  imasnopn  22749  imasncld  22750  imasncls  22751  qtopkgen  22769  basqtop  22770  tgqtop  22771  qtoprest  22776  kqsat  22790  kqcldsat  22792  kqnrmlem1  22802  kqnrmlem2  22803  hmeontr  22828  reghmph  22852  nrmhmph  22853  fmfnfmlem4  23016  fmfnfm  23017  flimopn  23034  flimclslem  23043  flfnei  23050  lmflf  23064  txflf  23065  fclsopn  23073  fclsfnflim  23086  alexsublem  23103  ptcmplem3  23113  cnextcn  23126  efmndtmd  23160  submtmd  23163  subgtgp  23164  symgtgp  23165  clssubg  23168  clsnsg  23169  tgpconncompeqg  23171  snclseqg  23175  tsmscls  23197  trust  23289  restutop  23297  restutopopn  23298  utop3cls  23311  utopreg  23312  trcfilu  23354  blssec  23496  prdsbl  23553  blssopn  23557  metcnp  23603  cfilucfil  23621  psmetutop  23629  iccntr  23890  icccmplem2  23892  reconnlem1  23895  metnrmlem1a  23927  metnrmlem1  23928  metnrmlem2  23929  metnrmlem3  23930  cnheibor  24024  lebnumlem1  24030  lebnumlem3  24032  lebnumii  24035  clsocv  24319  iscfil2  24335  iscmet3  24362  cmetss  24385  relcmpcmet  24387  bcthlem5  24397  itg1addlem5  24770  perfdvf  24972  dvres3  24982  dvres3a  24983  dvcmul  25013  dvcmulf  25014  dvlip2  25064  lhop1lem  25082  dvcnvrelem1  25086  dvcnvrelem2  25087  dvcnvre  25088  dvcvx  25089  plyco0  25258  plyaddlem1  25279  plymullem1  25280  aalioulem3  25399  ulmdvlem1  25464  axcontlem10  27244  eengtrkg  27257  wlkp1lem7  27949  1wlkdlem4  28405  hsupunss  29606  pjpjpre  29682  ssmd2  30575  superpos  30617  atexch  30644  curry2ima  30943  pfxf1  31118  gsumhashmul  31218  symgcom2  31255  pmtrcnelor  31262  cycpmco2lem7  31301  cycpmconjvlem  31310  cycpmconjv  31311  cyc3conja  31326  nsgmgc  31499  nsgqusf1olem3  31502  elrspunidl  31508  mxidlprm  31542  lssdimle  31593  dimkerim  31610  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  madjusmdetlem2  31680  zarclsun  31722  rhmpreimacnlem  31736  ordtconnlem1  31776  measiuns  32085  imambfm  32129  cnmbfm  32130  dya2iocnrect  32148  omsfval  32161  omssubaddlem  32166  omssubadd  32167  totprobd  32293  fzssfzo  32418  signstfvn  32448  bnj999  32838  bnj1408  32916  bnj1442  32929  bnj1450  32930  bnj1501  32947  fnrelpredd  32961  revwlk  32986  cvmsss2  33136  cvmliftmolem1  33143  cvmliftlem3  33149  cvmlift2lem9  33173  cvmlift2lem11  33175  cvmlift3lem6  33186  cvmlift3lem7  33187  ssmclslem  33427  mclsax  33431  mclsppslem  33445  mclspps  33446  dfrdg2  33677  ttrcltr  33702  neiin  34448  neibastop2  34477  filnetlem4  34497  rdgssun  35476  lindsdom  35698  poimirlem11  35715  poimirlem12  35716  itg2addnclem2  35756  cnres2  35848  sstotbnd2  35859  sstotbnd  35860  prdstotbnd  35879  heibor1lem  35894  igenval2  36151  lshpnelb  36925  lcvexchlem4  36978  lsatexch  36984  l1cvat  36996  lkrscss  37039  lkrss  37109  lkreqN  37111  paddunN  37868  osumcllem2N  37898  pmapojoinN  37909  pl42lem2N  37921  dibglbN  39107  diblss  39111  dicvaddcl  39131  dicvscacl  39132  diclss  39134  cdlemn5pre  39141  dihord5apre  39203  dihglblem3N  39236  dihglb2  39283  dochsat  39324  dochshpncl  39325  djhspss  39347  dihsumssj  39349  mapdlsm  39605  hdmaprnlem3eN  39799  hdmaplkr  39854  fnwe2lem2  40792  lnmlsslnm  40822  lmhmfgima  40825  hbtlem6  40870  trrelsuperreldg  41165  iunrelexpuztr  41216  clsk1indlem2  41541  grumnudlem  41792  dvsconst  41837  dvsinax  43344  dvbdfbdioolem1  43359  itgsinexplem1  43385  itgperiod  43412  stoweidlem39  43470  dirkeritg  43533  fourierdlem48  43585  fourierdlem49  43586  fourierdlem70  43607  fourierdlem71  43608  fourierdlem81  43618  issalgend  43767  f1oresf1o  44669  subsubmgm  45239  rmsuppss  45594  restcls2lem  46094  iscnrm3rlem7  46128