Theorem sseqtrrd 3971

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ss 3919

This theorem is used by:  3sstr4d  3989  fssrescdmd  7124  funfvima2d  7235  fnfvima  7236  frrlem8  8296  frrlem10  8298  fprresex  8313  oaordi  8537  omordi  8557  omlimcl  8569  oen0  8578  domunsncan  9079  f1opwfi  9327  cantnfle  9654  cantnflt  9655  cantnflem1d  9671  ttrcltr  9699  r1pwss  9770  rankxplim3  9867  acndom2  10061  fodomfi2  10067  cflm  10255  cflim2  10269  isf34lem5  10384  isf34lem7  10385  isf34lem6  10386  axdc2lem  10454  ttukeylem5  10519  wunex2  10751  ssfzunsn  13629  ccatass  14658  swrdval2  14718  splfv2a  14829  revccat  14839  cshimadifsn  14904  cshimadifsn0  14905  rtrclreclem1  15134  rtrclreclem2  15136  sumrblem  15801  prodrblem  16022  dfphi2  16871  vdwlem1  17079  basprssdmsets  17319  imasaddfnlem  17620  imasaddvallem  17621  imasvscafn  17629  imasvscaval  17630  mreexexlem4d  17741  mreexfidimd  17744  sscpwex  17910  acsmap2d  18649  gsumress  18790  subsubmgm  18818  subsubm  18931  frmdsssubm  18976  frmdss2  18978  subsubg  19279  cntzmhm2  19475  cntzcmnf  19978  ablcntzd  19990  gsumzsubmcl  20051  gsumconst  20067  gsumzmhm  20070  subgdmdprd  20169  dprdcntz2  20173  dprd2da  20177  dmdprdsplit2lem  20180  ablfac1eu  20208  pgpfaclem1  20216  pgpfaclem2  20217  subsubrng  20731  subsubrg  20766  issubdrg  20952  subdrgint  20975  lmhmlsp  21239  lspsntri  21287  lspindpi  21325  rspprop  21439  lidldvgen  21571  gsumfsum  21653  mrccss  21913  frlmsslsp  22015  lindsdom  22069  opsrtoslem2  22278  ressply1evl  22601  scmatsgrp1  22750  toponss  23158  ssntr  23289  elcls3  23314  toponmre  23324  neiptoptop  23362  neiptopnei  23363  neitr  23411  ordtbas  23423  ordtopn1  23425  ordtopn2  23426  iscnp3  23475  tgcn  23483  tgcnp  23484  ssidcn  23486  cnclsi  23503  cncls  23505  cncnp  23511  lmcld  23534  tgcmp  23632  cnconn  23653  connima  23656  clsconn  23661  conncompcld  23665  1stccnp  23694  kgentopon  23770  llycmpkgen2  23782  1stckgen  23786  kgencn2  23789  ptopn  23815  txcls  23836  ptpjcn  23843  ptclsg  23847  xkoccn  23851  txcnp  23852  ptcnplem  23853  txcmplem2  23874  xkoptsub  23886  xkopt  23887  xkoco2cn  23890  xkococnlem  23891  xkoinjcn  23919  imasnopn  23922  imasncld  23923  imasncls  23924  qtopkgen  23942  basqtop  23943  tgqtop  23944  qtoprest  23949  kqsat  23963  kqcldsat  23965  kqnrmlem1  23975  kqnrmlem2  23976  hmeontr  24001  reghmph  24025  nrmhmph  24026  fmfnfmlem4  24189  fmfnfm  24190  flimopn  24207  flimclslem  24216  flfnei  24223  lmflf  24237  txflf  24238  fclsopn  24246  fclsfnflim  24259  alexsublem  24276  ptcmplem3  24286  cnextcn  24299  efmndtmd  24333  submtmd  24336  subgtgp  24337  symgtgp  24338  clssubg  24341  clsnsg  24342  tgpconncompeqg  24344  snclseqg  24348  tsmscls  24370  trust  24461  restutop  24469  restutopopn  24470  utop3cls  24483  utopreg  24484  trcfilu  24525  blssec  24667  prdsbl  24723  blssopn  24727  metcnp  24773  cfilucfil  24791  psmetutop  24799  iccntr  25054  icccmplem2  25056  reconnlem1  25059  metnrmlem1a  25091  metnrmlem1  25092  metnrmlem2  25093  metnrmlem3  25094  cnheibor  25189  lebnumlem1  25195  lebnumlem3  25197  lebnumii  25200  clsocv  25484  iscfil2  25500  iscmet3  25527  cmetss  25550  relcmpcmet  25552  bcthlem5  25562  itg1addlem5  25934  perfdvf  26137  dvres3  26147  dvres3a  26148  dvcmul  26178  dvcmulf  26179  dvlip2  26229  lhop1lem  26247  dvcnvrelem1  26251  dvcnvrelem2  26252  dvcnvre  26253  dvcvx  26254  plyco0  26424  plyaddlem1  26446  plymullem1  26447  aalioulem3  26577  ulmdvlem1  26643  precsexlem6  28485  precsexlem7  28486  bdayn0p1  28642  bdaypw2n0bndlem  28736  z12bdaylem2  28744  plngrotlem1  29152  lnssplnglem  29156  prlngpln4  29323  quadcgrprlng  29331  axcontlem10  29438  eengtrkg  29451  wlkp1lem7  30145  revwlk  30154  cyclnumvtx  30275  1wlkdlem4  30618  hsupunss  31832  pjpjpre  31908  ssmd2  32801  superpos  32843  atexch  32870  curry2ima  33189  pfxf1  33396  gsumhashmul  33515  symgcom2  33532  pmtrcnelor  33539  cycpmco2lem7  33580  cycpmconjvlem  33589  cycpmconjv  33590  cyc3conja  33605  elrgspnsubrunlem2  33696  subsdrg  33747  nsgmgc  33849  nsgqusf1olem3  33852  elrspunidl  33864  mxidlprm  33881  rprmdvdsprod  33952  dfufd2lem  33967  esplyfvaln  34092  lssdimle  34126  dimkerim  34145  fedgmullem1  34147  fedgmullem2  34148  fedgmul  34149  dimlssid  34150  fldsdrgfldext2  34180  fldextrspunlsplem  34191  fldextrspunlsp  34192  fldextrspunlem1  34193  fldextrspundgdvdslem  34198  fldextrspundgdvds  34199  constr01  34260  constrmon  34262  constrextdg2lem  34266  constrext2chnlem  34268  madjusmdetlem2  34346  zarclsun  34388  rhmpreimacnlem  34402  ordtconnlem1  34442  measiuns  34736  imambfm  34781  cnmbfm  34782  dya2iocnrect  34800  omsfval  34813  omssubaddlem  34818  omssubadd  34819  totprobd  34945  fzssfzo  35058  signstfvn  35085  bnj999  35475  bnj1408  35553  bnj1442  35566  bnj1450  35567  bnj1501  35584  fnrelpredd  35604  cvmsss2  35861  cvmliftmolem1  35868  cvmliftlem3  35874  cvmlift2lem9  35898  cvmlift2lem11  35900  cvmlift3lem6  35911  cvmlift3lem7  35912  ssmclslem  36152  mclsax  36156  mclsppslem  36170  mclspps  36171  dfrdg2  36380  neiin  36959  neibastop2  36988  filnetlem4  37008  weiunfrlem  37091  rdgssun  38140  poimirlem11  38388  poimirlem12  38389  itg2addnclem2  38429  cnres2  38521  sstotbnd2  38532  sstotbnd  38533  prdstotbnd  38552  heibor1lem  38567  igenval2  38824  lshpnelb  39865  lcvexchlem4  39918  lsatexch  39924  l1cvat  39936  lkrscss  39979  lkrss  40049  lkreqN  40051  paddunN  40808  osumcllem2N  40838  pmapojoinN  40849  pl42lem2N  40861  dibglbN  42047  diblss  42051  dicvaddcl  42071  dicvscacl  42072  diclss  42074  cdlemn5pre  42081  dihord5apre  42143  dihglblem3N  42176  dihglb2  42223  dochsat  42264  dochshpncl  42265  djhspss  42287  dihsumssj  42289  mapdlsm  42545  hdmaprnlem3eN  42739  hdmaplkr  42794  fnwe2lem2  43900  lnmlsslnm  43930  lmhmfgima  43933  hbtlem6  43978  omabs2  44181  tfsconcatrev  44197  naddwordnexlem0  44245  trrelsuperreldg  44516  iunrelexpuztr  44567  clsk1indlem2  44890  grumnudlem  45117  dvsconst  45162  dvsinax  46749  dvbdfbdioolem1  46764  itgsinexplem1  46790  itgperiod  46817  stoweidlem39  46875  dirkeritg  46938  fourierdlem48  46990  fourierdlem49  46991  fourierdlem70  47012  fourierdlem71  47013  fourierdlem81  47023  issalgend  47174  chnsubseqwl  47715  tmachlem-agreeprod  47773  f1oresf1o  48186  clnbgrgrim  48858  rmsuppss  49308  restcls2lem  49847  iscnrm3rlem7  49880