Theorem sseqtrrd 3976

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

Syntax hints:   → wi 4   = wceq 1563   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924

This theorem is referenced by:  3sstr4d  3994  fssrescdmd  7112  funfvima2d  7220  fnfvima  7221  frrlem8  8278  frrlem10  8280  fprresex  8295  oaordi  8519  omordi  8539  omlimcl  8551  oen0  8560  domunsncan  9053  f1opwfi  9301  cantnfle  9628  cantnflt  9629  cantnflem1d  9645  ttrcltr  9673  r1pwss  9744  rankxplim3  9841  acndom2  10026  fodomfi2  10032  cflm  10221  cflim2  10235  isf34lem5  10350  isf34lem7  10351  isf34lem6  10352  axdc2lem  10420  ttukeylem5  10485  wunex2  10711  ssfzunsn  13589  ccatass  14616  swrdval2  14674  splfv2a  14783  revccat  14793  cshimadifsn  14856  cshimadifsn0  14857  rtrclreclem1  15084  rtrclreclem2  15086  sumrblem  15752  prodrblem  15973  dfphi2  16823  vdwlem1  17031  basprssdmsets  17271  imasaddfnlem  17572  imasaddvallem  17573  imasvscafn  17581  imasvscaval  17582  mreexexlem4d  17693  mreexfidimd  17696  sscpwex  17862  acsmap2d  18601  gsumress  18730  subsubmgm  18758  subsubm  18865  frmdsssubm  18910  frmdss2  18912  subsubg  19207  cntzmhm2  19403  cntzcmnf  19906  ablcntzd  19918  gsumzsubmcl  19979  gsumconst  19995  gsumzmhm  19998  subgdmdprd  20097  dprdcntz2  20101  dprd2da  20105  dmdprdsplit2lem  20108  ablfac1eu  20136  pgpfaclem1  20144  pgpfaclem2  20145  subsubrng  20639  subsubrg  20674  issubdrg  20852  subdrgint  20875  lmhmlsp  21139  lspsntri  21187  lspindpi  21225  lidldvgen  21462  gsumfsum  21544  mrccss  21804  frlmsslsp  21906  opsrtoslem2  22167  ressply1evl  22491  scmatsgrp1  22640  toponss  23045  ssntr  23176  elcls3  23201  toponmre  23211  neiptoptop  23249  neiptopnei  23250  neitr  23298  ordtbas  23310  ordtopn1  23312  ordtopn2  23313  iscnp3  23362  tgcn  23370  tgcnp  23371  ssidcn  23373  cnclsi  23390  cncls  23392  cncnp  23398  lmcld  23421  tgcmp  23519  cnconn  23540  connima  23543  clsconn  23548  conncompcld  23552  1stccnp  23580  kgentopon  23656  llycmpkgen2  23668  1stckgen  23672  kgencn2  23675  ptopn  23701  txcls  23722  ptpjcn  23729  ptclsg  23733  xkoccn  23737  txcnp  23738  ptcnplem  23739  txcmplem2  23760  xkoptsub  23772  xkopt  23773  xkoco2cn  23776  xkococnlem  23777  xkoinjcn  23805  imasnopn  23808  imasncld  23809  imasncls  23810  qtopkgen  23828  basqtop  23829  tgqtop  23830  qtoprest  23835  kqsat  23849  kqcldsat  23851  kqnrmlem1  23861  kqnrmlem2  23862  hmeontr  23887  reghmph  23911  nrmhmph  23912  fmfnfmlem4  24075  fmfnfm  24076  flimopn  24093  flimclslem  24102  flfnei  24109  lmflf  24123  txflf  24124  fclsopn  24132  fclsfnflim  24145  alexsublem  24162  ptcmplem3  24172  cnextcn  24185  efmndtmd  24219  submtmd  24222  subgtgp  24223  symgtgp  24224  clssubg  24227  clsnsg  24228  tgpconncompeqg  24230  snclseqg  24234  tsmscls  24256  trust  24347  restutop  24355  restutopopn  24356  utop3cls  24369  utopreg  24370  trcfilu  24411  blssec  24553  prdsbl  24609  blssopn  24613  metcnp  24659  cfilucfil  24677  psmetutop  24685  iccntr  24940  icccmplem2  24942  reconnlem1  24945  metnrmlem1a  24977  metnrmlem1  24978  metnrmlem2  24979  metnrmlem3  24980  cnheibor  25075  lebnumlem1  25081  lebnumlem3  25083  lebnumii  25086  clsocv  25370  iscfil2  25386  iscmet3  25413  cmetss  25436  relcmpcmet  25438  bcthlem5  25448  itg1addlem5  25820  perfdvf  26023  dvres3  26033  dvres3a  26034  dvcmul  26064  dvcmulf  26065  dvlip2  26115  lhop1lem  26133  dvcnvrelem1  26137  dvcnvrelem2  26138  dvcnvre  26139  dvcvx  26140  plyco0  26310  plyaddlem1  26331  plymullem1  26332  aalioulem3  26456  ulmdvlem1  26521  precsexlem6  28363  precsexlem7  28364  bdayn0p1  28520  bdaypw2n0bndlem  28614  z12bdaylem2  28622  plngrotlem1  29017  lnssplnglem  29021  axcontlem10  29232  eengtrkg  29245  wlkp1lem7  29936  cyclnumvtx  30058  1wlkdlem4  30400  hsupunss  31604  pjpjpre  31680  ssmd2  32573  superpos  32615  atexch  32642  curry2ima  32966  pfxf1  33175  gsumhashmul  33300  symgcom2  33317  pmtrcnelor  33324  cycpmco2lem7  33365  cycpmconjvlem  33374  cycpmconjv  33375  cyc3conja  33390  elrgspnsubrunlem2  33481  subsdrg  33534  nsgmgc  33637  nsgqusf1olem3  33640  elrspunidl  33652  mxidlprm  33670  rprmdvdsprod  33741  dfufd2lem  33756  esplyfvaln  33881  lssdimle  33915  dimkerim  33934  fedgmullem1  33936  fedgmullem2  33937  fedgmul  33938  dimlssid  33939  fldsdrgfldext2  33969  fldextrspunlsplem  33980  fldextrspunlsp  33981  fldextrspunlem1  33982  fldextrspundgdvdslem  33987  fldextrspundgdvds  33988  constr01  34049  constrmon  34051  constrextdg2lem  34055  constrext2chnlem  34057  madjusmdetlem2  34135  zarclsun  34177  rhmpreimacnlem  34191  ordtconnlem1  34231  measiuns  34524  imambfm  34569  cnmbfm  34570  dya2iocnrect  34588  omsfval  34601  omssubaddlem  34606  omssubadd  34607  totprobd  34733  fzssfzo  34846  signstfvn  34873  bnj999  35263  bnj1408  35341  bnj1442  35354  bnj1450  35355  bnj1501  35372  fnrelpredd  35397  revwlk  35488  cvmsss2  35637  cvmliftmolem1  35644  cvmliftlem3  35650  cvmlift2lem9  35674  cvmlift2lem11  35676  cvmlift3lem6  35687  cvmlift3lem7  35688  ssmclslem  35928  mclsax  35932  mclsppslem  35946  mclspps  35947  dfrdg2  36156  neiin  36705  neibastop2  36734  filnetlem4  36754  weiunfrlem  36837  rdgssun  37884  lindsdom  38125  poimirlem11  38142  poimirlem12  38143  itg2addnclem2  38183  cnres2  38274  sstotbnd2  38285  sstotbnd  38286  prdstotbnd  38305  heibor1lem  38320  igenval2  38577  lshpnelb  39620  lcvexchlem4  39673  lsatexch  39679  l1cvat  39691  lkrscss  39734  lkrss  39804  lkreqN  39806  paddunN  40563  osumcllem2N  40593  pmapojoinN  40604  pl42lem2N  40616  dibglbN  41802  diblss  41806  dicvaddcl  41826  dicvscacl  41827  diclss  41829  cdlemn5pre  41836  dihord5apre  41898  dihglblem3N  41931  dihglb2  41978  dochsat  42019  dochshpncl  42020  djhspss  42042  dihsumssj  42044  mapdlsm  42300  hdmaprnlem3eN  42494  hdmaplkr  42549  fnwe2lem2  43640  lnmlsslnm  43670  lmhmfgima  43673  hbtlem6  43718  omabs2  43921  tfsconcatrev  43937  naddwordnexlem0  43985  trrelsuperreldg  44256  iunrelexpuztr  44307  clsk1indlem2  44630  grumnudlem  44859  dvsconst  44904  dvsinax  46485  dvbdfbdioolem1  46500  itgsinexplem1  46526  itgperiod  46553  stoweidlem39  46611  dirkeritg  46674  fourierdlem48  46726  fourierdlem49  46727  fourierdlem70  46748  fourierdlem71  46749  fourierdlem81  46759  issalgend  46910  chnsubseqwl  47453  f1oresf1o  47882  clnbgrgrim  48554  rmsuppss  49001  restcls2lem  49542  iscnrm3rlem7  49575