Theorem sseqtrrd 4021

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

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

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968

This theorem is referenced by:  3sstr4d  4039  fssrescdmd  7146  funfvima2d  7252  fnfvima  7253  frrlem8  8318  frrlem10  8320  fprresex  8335  wfrlem17OLD  8365  oaordi  8584  omordi  8604  omlimcl  8616  oen0  8624  domunsncan  9112  f1opwfi  9396  cantnfle  9711  cantnflt  9712  cantnflem1d  9728  ttrcltr  9756  r1pwss  9824  rankxplim3  9921  acndom2  10094  fodomfi2  10100  cflm  10290  cflim2  10303  isf34lem5  10418  isf34lem7  10419  isf34lem6  10420  axdc2lem  10488  ttukeylem5  10553  wunex2  10778  ssfzunsn  13610  ccatass  14626  swrdval2  14684  splfv2a  14794  revccat  14804  cshimadifsn  14868  cshimadifsn0  14869  rtrclreclem1  15096  rtrclreclem2  15098  sumrblem  15747  prodrblem  15965  dfphi2  16811  vdwlem1  17019  basprssdmsets  17259  imasaddfnlem  17573  imasaddvallem  17574  imasvscafn  17582  imasvscaval  17583  mreexexlem4d  17690  mreexfidimd  17693  sscpwex  17859  acsmap2d  18600  gsumress  18695  subsubmgm  18723  subsubm  18829  frmdsssubm  18874  frmdss2  18876  subsubg  19167  cntzmhm2  19360  cntzcmnf  19863  ablcntzd  19875  gsumzsubmcl  19936  gsumconst  19952  gsumzmhm  19955  subgdmdprd  20054  dprdcntz2  20058  dprd2da  20062  dmdprdsplit2lem  20065  ablfac1eu  20093  pgpfaclem1  20101  pgpfaclem2  20102  subsubrng  20563  subsubrg  20598  issubdrg  20781  subdrgint  20804  lmhmlsp  21048  lspsntri  21096  lspindpi  21134  lidldvgen  21344  gsumfsum  21452  mrccss  21712  frlmsslsp  21816  opsrtoslem2  22080  ressply1evl  22374  scmatsgrp1  22528  toponss  22933  ssntr  23066  elcls3  23091  toponmre  23101  neiptoptop  23139  neiptopnei  23140  neitr  23188  ordtbas  23200  ordtopn1  23202  ordtopn2  23203  iscnp3  23252  tgcn  23260  tgcnp  23261  ssidcn  23263  cnclsi  23280  cncls  23282  cncnp  23288  lmcld  23311  tgcmp  23409  cnconn  23430  connima  23433  clsconn  23438  conncompcld  23442  1stccnp  23470  kgentopon  23546  llycmpkgen2  23558  1stckgen  23562  kgencn2  23565  ptopn  23591  txcls  23612  ptpjcn  23619  ptclsg  23623  xkoccn  23627  txcnp  23628  ptcnplem  23629  txcmplem2  23650  xkoptsub  23662  xkopt  23663  xkoco2cn  23666  xkococnlem  23667  xkoinjcn  23695  imasnopn  23698  imasncld  23699  imasncls  23700  qtopkgen  23718  basqtop  23719  tgqtop  23720  qtoprest  23725  kqsat  23739  kqcldsat  23741  kqnrmlem1  23751  kqnrmlem2  23752  hmeontr  23777  reghmph  23801  nrmhmph  23802  fmfnfmlem4  23965  fmfnfm  23966  flimopn  23983  flimclslem  23992  flfnei  23999  lmflf  24013  txflf  24014  fclsopn  24022  fclsfnflim  24035  alexsublem  24052  ptcmplem3  24062  cnextcn  24075  efmndtmd  24109  submtmd  24112  subgtgp  24113  symgtgp  24114  clssubg  24117  clsnsg  24118  tgpconncompeqg  24120  snclseqg  24124  tsmscls  24146  trust  24238  restutop  24246  restutopopn  24247  utop3cls  24260  utopreg  24261  trcfilu  24303  blssec  24445  prdsbl  24504  blssopn  24508  metcnp  24554  cfilucfil  24572  psmetutop  24580  iccntr  24843  icccmplem2  24845  reconnlem1  24848  metnrmlem1a  24880  metnrmlem1  24881  metnrmlem2  24882  metnrmlem3  24883  cnheibor  24987  lebnumlem1  24993  lebnumlem3  24995  lebnumii  24998  clsocv  25284  iscfil2  25300  iscmet3  25327  cmetss  25350  relcmpcmet  25352  bcthlem5  25362  itg1addlem5  25735  perfdvf  25938  dvres3  25948  dvres3a  25949  dvcmul  25981  dvcmulf  25982  dvlip2  26034  lhop1lem  26052  dvcnvrelem1  26056  dvcnvrelem2  26057  dvcnvre  26058  dvcvx  26059  plyco0  26231  plyaddlem1  26252  plymullem1  26253  aalioulem3  26376  ulmdvlem1  26443  precsexlem6  28236  precsexlem7  28237  axcontlem10  28988  eengtrkg  29001  wlkp1lem7  29697  cyclnumvtx  29820  1wlkdlem4  30159  hsupunss  31362  pjpjpre  31438  ssmd2  32331  superpos  32373  atexch  32400  curry2ima  32718  pfxf1  32926  gsumhashmul  33064  symgcom2  33104  pmtrcnelor  33111  cycpmco2lem7  33152  cycpmconjvlem  33161  cycpmconjv  33162  cyc3conja  33177  elrgspnsubrunlem2  33252  nsgmgc  33440  nsgqusf1olem3  33443  elrspunidl  33456  mxidlprm  33498  rprmdvdsprod  33562  dfufd2lem  33577  lssdimle  33658  dimkerim  33678  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  dimlssid  33683  fldsdrgfldext2  33713  fldextrspunlsplem  33723  fldextrspunlsp  33724  fldextrspunlem1  33725  fldextrspundgdvdslem  33730  fldextrspundgdvds  33731  constr01  33783  constrmon  33785  constrextdg2lem  33789  madjusmdetlem2  33827  zarclsun  33869  rhmpreimacnlem  33883  ordtconnlem1  33923  measiuns  34218  imambfm  34264  cnmbfm  34265  dya2iocnrect  34283  omsfval  34296  omssubaddlem  34301  omssubadd  34302  totprobd  34428  fzssfzo  34554  signstfvn  34584  bnj999  34972  bnj1408  35050  bnj1442  35063  bnj1450  35064  bnj1501  35081  fnrelpredd  35103  revwlk  35130  cvmsss2  35279  cvmliftmolem1  35286  cvmliftlem3  35292  cvmlift2lem9  35316  cvmlift2lem11  35318  cvmlift3lem6  35329  cvmlift3lem7  35330  ssmclslem  35570  mclsax  35574  mclsppslem  35588  mclspps  35589  dfrdg2  35796  neiin  36333  neibastop2  36362  filnetlem4  36382  weiunfrlem  36465  rdgssun  37379  lindsdom  37621  poimirlem11  37638  poimirlem12  37639  itg2addnclem2  37679  cnres2  37770  sstotbnd2  37781  sstotbnd  37782  prdstotbnd  37801  heibor1lem  37816  igenval2  38073  lshpnelb  38985  lcvexchlem4  39038  lsatexch  39044  l1cvat  39056  lkrscss  39099  lkrss  39169  lkreqN  39171  paddunN  39929  osumcllem2N  39959  pmapojoinN  39970  pl42lem2N  39982  dibglbN  41168  diblss  41172  dicvaddcl  41192  dicvscacl  41193  diclss  41195  cdlemn5pre  41202  dihord5apre  41264  dihglblem3N  41297  dihglb2  41344  dochsat  41385  dochshpncl  41386  djhspss  41408  dihsumssj  41410  mapdlsm  41666  hdmaprnlem3eN  41860  hdmaplkr  41915  fnwe2lem2  43063  lnmlsslnm  43093  lmhmfgima  43096  hbtlem6  43141  omabs2  43345  tfsconcatrev  43361  naddwordnexlem0  43409  trrelsuperreldg  43681  iunrelexpuztr  43732  clsk1indlem2  44055  grumnudlem  44304  dvsconst  44349  dvsinax  45928  dvbdfbdioolem1  45943  itgsinexplem1  45969  itgperiod  45996  stoweidlem39  46054  dirkeritg  46117  fourierdlem48  46169  fourierdlem49  46170  fourierdlem70  46191  fourierdlem71  46192  fourierdlem81  46202  issalgend  46353  f1oresf1o  47302  clnbgrgrim  47902  rmsuppss  48286  restcls2lem  48810  iscnrm3rlem7  48843