Theorem sseqtrrd 3972

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3919

This theorem is referenced by:  3sstr4d  3990  fssrescdmd  7059  funfvima2d  7166  fnfvima  7167  frrlem8  8223  frrlem10  8225  fprresex  8240  oaordi  8461  omordi  8481  omlimcl  8493  oen0  8501  domunsncan  8990  f1opwfi  9240  cantnfle  9561  cantnflt  9562  cantnflem1d  9578  ttrcltr  9606  r1pwss  9674  rankxplim3  9771  acndom2  9942  fodomfi2  9948  cflm  10138  cflim2  10151  isf34lem5  10266  isf34lem7  10267  isf34lem6  10268  axdc2lem  10336  ttukeylem5  10401  wunex2  10626  ssfzunsn  13467  ccatass  14493  swrdval2  14551  splfv2a  14660  revccat  14670  cshimadifsn  14733  cshimadifsn0  14734  rtrclreclem1  14961  rtrclreclem2  14963  sumrblem  15615  prodrblem  15833  dfphi2  16682  vdwlem1  16890  basprssdmsets  17129  imasaddfnlem  17429  imasaddvallem  17430  imasvscafn  17438  imasvscaval  17439  mreexexlem4d  17550  mreexfidimd  17553  sscpwex  17719  acsmap2d  18458  gsumress  18587  subsubmgm  18615  subsubm  18721  frmdsssubm  18766  frmdss2  18768  subsubg  19059  cntzmhm2  19252  cntzcmnf  19755  ablcntzd  19767  gsumzsubmcl  19828  gsumconst  19844  gsumzmhm  19847  subgdmdprd  19946  dprdcntz2  19950  dprd2da  19954  dmdprdsplit2lem  19957  ablfac1eu  19985  pgpfaclem1  19993  pgpfaclem2  19994  subsubrng  20476  subsubrg  20511  issubdrg  20693  subdrgint  20716  lmhmlsp  20981  lspsntri  21029  lspindpi  21067  lidldvgen  21269  gsumfsum  21369  mrccss  21629  frlmsslsp  21731  opsrtoslem2  21989  ressply1evl  22283  scmatsgrp1  22435  toponss  22840  ssntr  22971  elcls3  22996  toponmre  23006  neiptoptop  23044  neiptopnei  23045  neitr  23093  ordtbas  23105  ordtopn1  23107  ordtopn2  23108  iscnp3  23157  tgcn  23165  tgcnp  23166  ssidcn  23168  cnclsi  23185  cncls  23187  cncnp  23193  lmcld  23216  tgcmp  23314  cnconn  23335  connima  23338  clsconn  23343  conncompcld  23347  1stccnp  23375  kgentopon  23451  llycmpkgen2  23463  1stckgen  23467  kgencn2  23470  ptopn  23496  txcls  23517  ptpjcn  23524  ptclsg  23528  xkoccn  23532  txcnp  23533  ptcnplem  23534  txcmplem2  23555  xkoptsub  23567  xkopt  23568  xkoco2cn  23571  xkococnlem  23572  xkoinjcn  23600  imasnopn  23603  imasncld  23604  imasncls  23605  qtopkgen  23623  basqtop  23624  tgqtop  23625  qtoprest  23630  kqsat  23644  kqcldsat  23646  kqnrmlem1  23656  kqnrmlem2  23657  hmeontr  23682  reghmph  23706  nrmhmph  23707  fmfnfmlem4  23870  fmfnfm  23871  flimopn  23888  flimclslem  23897  flfnei  23904  lmflf  23918  txflf  23919  fclsopn  23927  fclsfnflim  23940  alexsublem  23957  ptcmplem3  23967  cnextcn  23980  efmndtmd  24014  submtmd  24017  subgtgp  24018  symgtgp  24019  clssubg  24022  clsnsg  24023  tgpconncompeqg  24025  snclseqg  24029  tsmscls  24051  trust  24142  restutop  24150  restutopopn  24151  utop3cls  24164  utopreg  24165  trcfilu  24206  blssec  24348  prdsbl  24404  blssopn  24408  metcnp  24454  cfilucfil  24472  psmetutop  24480  iccntr  24735  icccmplem2  24737  reconnlem1  24740  metnrmlem1a  24772  metnrmlem1  24773  metnrmlem2  24774  metnrmlem3  24775  cnheibor  24879  lebnumlem1  24885  lebnumlem3  24887  lebnumii  24890  clsocv  25175  iscfil2  25191  iscmet3  25218  cmetss  25241  relcmpcmet  25243  bcthlem5  25253  itg1addlem5  25626  perfdvf  25829  dvres3  25839  dvres3a  25840  dvcmul  25872  dvcmulf  25873  dvlip2  25925  lhop1lem  25943  dvcnvrelem1  25947  dvcnvrelem2  25948  dvcnvre  25949  dvcvx  25950  plyco0  26122  plyaddlem1  26143  plymullem1  26144  aalioulem3  26267  ulmdvlem1  26334  precsexlem6  28148  precsexlem7  28149  bdayn0p1  28292  axcontlem10  28949  eengtrkg  28962  wlkp1lem7  29654  cyclnumvtx  29776  1wlkdlem4  30115  hsupunss  31318  pjpjpre  31394  ssmd2  32287  superpos  32329  atexch  32356  curry2ima  32685  pfxf1  32918  gsumhashmul  33036  symgcom2  33048  pmtrcnelor  33055  cycpmco2lem7  33096  cycpmconjvlem  33105  cycpmconjv  33106  cyc3conja  33121  elrgspnsubrunlem2  33210  subsdrg  33259  nsgmgc  33372  nsgqusf1olem3  33375  elrspunidl  33388  mxidlprm  33430  rprmdvdsprod  33494  dfufd2lem  33509  lssdimle  33615  dimkerim  33635  fedgmullem1  33637  fedgmullem2  33638  fedgmul  33639  dimlssid  33640  fldsdrgfldext2  33670  fldextrspunlsplem  33681  fldextrspunlsp  33682  fldextrspunlem1  33683  fldextrspundgdvdslem  33688  fldextrspundgdvds  33689  constr01  33750  constrmon  33752  constrextdg2lem  33756  constrext2chnlem  33758  madjusmdetlem2  33836  zarclsun  33878  rhmpreimacnlem  33892  ordtconnlem1  33932  measiuns  34225  imambfm  34270  cnmbfm  34271  dya2iocnrect  34289  omsfval  34302  omssubaddlem  34307  omssubadd  34308  totprobd  34434  fzssfzo  34547  signstfvn  34577  bnj999  34965  bnj1408  35043  bnj1442  35056  bnj1450  35057  bnj1501  35074  fnrelpredd  35097  revwlk  35157  cvmsss2  35306  cvmliftmolem1  35313  cvmliftlem3  35319  cvmlift2lem9  35343  cvmlift2lem11  35345  cvmlift3lem6  35356  cvmlift3lem7  35357  ssmclslem  35597  mclsax  35601  mclsppslem  35615  mclspps  35616  dfrdg2  35828  neiin  36365  neibastop2  36394  filnetlem4  36414  weiunfrlem  36497  rdgssun  37411  lindsdom  37653  poimirlem11  37670  poimirlem12  37671  itg2addnclem2  37711  cnres2  37802  sstotbnd2  37813  sstotbnd  37814  prdstotbnd  37833  heibor1lem  37848  igenval2  38105  lshpnelb  39022  lcvexchlem4  39075  lsatexch  39081  l1cvat  39093  lkrscss  39136  lkrss  39206  lkreqN  39208  paddunN  39965  osumcllem2N  39995  pmapojoinN  40006  pl42lem2N  40018  dibglbN  41204  diblss  41208  dicvaddcl  41228  dicvscacl  41229  diclss  41231  cdlemn5pre  41238  dihord5apre  41300  dihglblem3N  41333  dihglb2  41380  dochsat  41421  dochshpncl  41422  djhspss  41444  dihsumssj  41446  mapdlsm  41702  hdmaprnlem3eN  41896  hdmaplkr  41951  fnwe2lem2  43083  lnmlsslnm  43113  lmhmfgima  43116  hbtlem6  43161  omabs2  43364  tfsconcatrev  43380  naddwordnexlem0  43428  trrelsuperreldg  43700  iunrelexpuztr  43751  clsk1indlem2  44074  grumnudlem  44317  dvsconst  44362  dvsinax  45950  dvbdfbdioolem1  45965  itgsinexplem1  45991  itgperiod  46018  stoweidlem39  46076  dirkeritg  46139  fourierdlem48  46191  fourierdlem49  46192  fourierdlem70  46213  fourierdlem71  46214  fourierdlem81  46224  issalgend  46375  f1oresf1o  47320  clnbgrgrim  47964  rmsuppss  48400  restcls2lem  48943  iscnrm3rlem7  48976