Theorem sseqtrrd 4015

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

Syntax hints:   → wi 4   = wceq 1533   ⊆ wss 3940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3947  df-ss 3957

This theorem is referenced by:  funfvima2d  7225  fnfvima  7226  frrlem8  8273  frrlem10  8275  fprresex  8290  wfrlem17OLD  8320  oaordi  8541  omordi  8561  omlimcl  8573  oen0  8581  domunsncan  9067  f1opwfi  9351  cantnfle  9661  cantnflt  9662  cantnflem1d  9678  ttrcltr  9706  r1pwss  9774  rankxplim3  9871  acndom2  10044  fodomfi2  10050  cflm  10240  cflim2  10253  isf34lem5  10368  isf34lem7  10369  isf34lem6  10370  axdc2lem  10438  ttukeylem5  10503  wunex2  10728  ssfzunsn  13543  ccatass  14534  swrdval2  14592  splfv2a  14702  revccat  14712  cshimadifsn  14776  cshimadifsn0  14777  rtrclreclem1  15000  rtrclreclem2  15002  sumrblem  15653  prodrblem  15869  dfphi2  16703  vdwlem1  16910  basprssdmsets  17153  imasaddfnlem  17470  imasaddvallem  17471  imasvscafn  17479  imasvscaval  17480  mreexexlem4d  17587  mreexfidimd  17590  sscpwex  17758  acsmap2d  18507  gsumress  18602  subsubmgm  18630  subsubm  18728  frmdsssubm  18773  frmdss2  18775  subsubg  19061  cntzmhm2  19243  cntzcmnf  19750  ablcntzd  19762  gsumzsubmcl  19823  gsumconst  19839  gsumzmhm  19842  subgdmdprd  19941  dprdcntz2  19945  dprd2da  19949  dmdprdsplit2lem  19952  ablfac1eu  19980  pgpfaclem1  19988  pgpfaclem2  19989  subsubrng  20448  subsubrg  20485  issubdrg  20616  subdrgint  20639  lmhmlsp  20882  lspsntri  20930  lspindpi  20968  lidldvgen  21172  gsumfsum  21291  mrccss  21547  frlmsslsp  21651  opsrtoslem2  21918  scmatsgrp1  22334  toponss  22739  ssntr  22872  elcls3  22897  toponmre  22907  neiptoptop  22945  neiptopnei  22946  neitr  22994  ordtbas  23006  ordtopn1  23008  ordtopn2  23009  iscnp3  23058  tgcn  23066  tgcnp  23067  ssidcn  23069  cnclsi  23086  cncls  23088  cncnp  23094  lmcld  23117  tgcmp  23215  cnconn  23236  connima  23239  clsconn  23244  conncompcld  23248  1stccnp  23276  kgentopon  23352  llycmpkgen2  23364  1stckgen  23368  kgencn2  23371  ptopn  23397  txcls  23418  ptpjcn  23425  ptclsg  23429  xkoccn  23433  txcnp  23434  ptcnplem  23435  txcmplem2  23456  xkoptsub  23468  xkopt  23469  xkoco2cn  23472  xkococnlem  23473  xkoinjcn  23501  imasnopn  23504  imasncld  23505  imasncls  23506  qtopkgen  23524  basqtop  23525  tgqtop  23526  qtoprest  23531  kqsat  23545  kqcldsat  23547  kqnrmlem1  23557  kqnrmlem2  23558  hmeontr  23583  reghmph  23607  nrmhmph  23608  fmfnfmlem4  23771  fmfnfm  23772  flimopn  23789  flimclslem  23798  flfnei  23805  lmflf  23819  txflf  23820  fclsopn  23828  fclsfnflim  23841  alexsublem  23858  ptcmplem3  23868  cnextcn  23881  efmndtmd  23915  submtmd  23918  subgtgp  23919  symgtgp  23920  clssubg  23923  clsnsg  23924  tgpconncompeqg  23926  snclseqg  23930  tsmscls  23952  trust  24044  restutop  24052  restutopopn  24053  utop3cls  24066  utopreg  24067  trcfilu  24109  blssec  24251  prdsbl  24310  blssopn  24314  metcnp  24360  cfilucfil  24378  psmetutop  24386  iccntr  24647  icccmplem2  24649  reconnlem1  24652  metnrmlem1a  24684  metnrmlem1  24685  metnrmlem2  24686  metnrmlem3  24687  cnheibor  24791  lebnumlem1  24797  lebnumlem3  24799  lebnumii  24802  clsocv  25088  iscfil2  25104  iscmet3  25131  cmetss  25154  relcmpcmet  25156  bcthlem5  25166  itg1addlem5  25540  perfdvf  25742  dvres3  25752  dvres3a  25753  dvcmul  25785  dvcmulf  25786  dvlip2  25838  lhop1lem  25856  dvcnvrelem1  25860  dvcnvrelem2  25861  dvcnvre  25862  dvcvx  25863  plyco0  26034  plyaddlem1  26055  plymullem1  26056  aalioulem3  26176  ulmdvlem1  26241  precsexlem6  28014  precsexlem7  28015  axcontlem10  28655  eengtrkg  28668  wlkp1lem7  29360  1wlkdlem4  29817  hsupunss  31020  pjpjpre  31096  ssmd2  31989  superpos  32031  atexch  32058  curry2ima  32354  pfxf1  32532  gsumhashmul  32635  symgcom2  32672  pmtrcnelor  32679  cycpmco2lem7  32718  cycpmconjvlem  32727  cycpmconjv  32728  cyc3conja  32743  nsgmgc  32954  nsgqusf1olem3  32957  elrspunidl  32977  mxidlprm  33017  ressply1evl  33078  lssdimle  33137  dimkerim  33157  fedgmullem1  33159  fedgmullem2  33160  fedgmul  33161  madjusmdetlem2  33263  zarclsun  33305  rhmpreimacnlem  33319  ordtconnlem1  33359  measiuns  33670  imambfm  33716  cnmbfm  33717  dya2iocnrect  33735  omsfval  33748  omssubaddlem  33753  omssubadd  33754  totprobd  33880  fzssfzo  34005  signstfvn  34035  bnj999  34424  bnj1408  34502  bnj1442  34515  bnj1450  34516  bnj1501  34533  fnrelpredd  34547  revwlk  34570  cvmsss2  34720  cvmliftmolem1  34727  cvmliftlem3  34733  cvmlift2lem9  34757  cvmlift2lem11  34759  cvmlift3lem6  34770  cvmlift3lem7  34771  ssmclslem  35011  mclsax  35015  mclsppslem  35029  mclspps  35030  dfrdg2  35228  neiin  35673  neibastop2  35702  filnetlem4  35722  rdgssun  36715  lindsdom  36938  poimirlem11  36955  poimirlem12  36956  itg2addnclem2  36996  cnres2  37087  sstotbnd2  37098  sstotbnd  37099  prdstotbnd  37118  heibor1lem  37133  igenval2  37390  lshpnelb  38310  lcvexchlem4  38363  lsatexch  38369  l1cvat  38381  lkrscss  38424  lkrss  38494  lkreqN  38496  paddunN  39254  osumcllem2N  39284  pmapojoinN  39295  pl42lem2N  39307  dibglbN  40493  diblss  40497  dicvaddcl  40517  dicvscacl  40518  diclss  40520  cdlemn5pre  40527  dihord5apre  40589  dihglblem3N  40622  dihglb2  40669  dochsat  40710  dochshpncl  40711  djhspss  40733  dihsumssj  40735  mapdlsm  40991  hdmaprnlem3eN  41185  hdmaplkr  41240  fnwe2lem2  42248  lnmlsslnm  42278  lmhmfgima  42281  hbtlem6  42326  omabs2  42537  tfsconcatrev  42553  naddwordnexlem0  42602  trrelsuperreldg  42874  iunrelexpuztr  42925  clsk1indlem2  43248  grumnudlem  43499  dvsconst  43544  dvsinax  45080  dvbdfbdioolem1  45095  itgsinexplem1  45121  itgperiod  45148  stoweidlem39  45206  dirkeritg  45269  fourierdlem48  45321  fourierdlem49  45322  fourierdlem70  45343  fourierdlem71  45344  fourierdlem81  45354  issalgend  45505  f1oresf1o  46449  rmsuppss  47201  restcls2lem  47699  iscnrm3rlem7  47733