Theorem sseqtrrd 3959

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  3sstr4d  3977  fssrescdmd  7079  funfvima2d  7187  fnfvima  7188  frrlem8  8243  frrlem10  8245  fprresex  8260  oaordi  8481  omordi  8501  omlimcl  8513  oen0  8522  domunsncan  9015  f1opwfi  9266  cantnfle  9592  cantnflt  9593  cantnflem1d  9609  ttrcltr  9637  r1pwss  9708  rankxplim3  9805  acndom2  9976  fodomfi2  9982  cflm  10172  cflim2  10185  isf34lem5  10300  isf34lem7  10301  isf34lem6  10302  axdc2lem  10370  ttukeylem5  10435  wunex2  10661  ssfzunsn  13524  ccatass  14551  swrdval2  14609  splfv2a  14718  revccat  14728  cshimadifsn  14791  cshimadifsn0  14792  rtrclreclem1  15019  rtrclreclem2  15021  sumrblem  15673  prodrblem  15894  dfphi2  16744  vdwlem1  16952  basprssdmsets  17191  imasaddfnlem  17492  imasaddvallem  17493  imasvscafn  17501  imasvscaval  17502  mreexexlem4d  17613  mreexfidimd  17616  sscpwex  17782  acsmap2d  18521  gsumress  18650  subsubmgm  18678  subsubm  18784  frmdsssubm  18829  frmdss2  18831  subsubg  19125  cntzmhm2  19317  cntzcmnf  19820  ablcntzd  19832  gsumzsubmcl  19893  gsumconst  19909  gsumzmhm  19912  subgdmdprd  20011  dprdcntz2  20015  dprd2da  20019  dmdprdsplit2lem  20022  ablfac1eu  20050  pgpfaclem1  20058  pgpfaclem2  20059  subsubrng  20540  subsubrg  20575  issubdrg  20757  subdrgint  20780  lmhmlsp  21044  lspsntri  21092  lspindpi  21130  lidldvgen  21332  gsumfsum  21414  mrccss  21674  frlmsslsp  21776  opsrtoslem2  22034  ressply1evl  22335  scmatsgrp1  22487  toponss  22892  ssntr  23023  elcls3  23048  toponmre  23058  neiptoptop  23096  neiptopnei  23097  neitr  23145  ordtbas  23157  ordtopn1  23159  ordtopn2  23160  iscnp3  23209  tgcn  23217  tgcnp  23218  ssidcn  23220  cnclsi  23237  cncls  23239  cncnp  23245  lmcld  23268  tgcmp  23366  cnconn  23387  connima  23390  clsconn  23395  conncompcld  23399  1stccnp  23427  kgentopon  23503  llycmpkgen2  23515  1stckgen  23519  kgencn2  23522  ptopn  23548  txcls  23569  ptpjcn  23576  ptclsg  23580  xkoccn  23584  txcnp  23585  ptcnplem  23586  txcmplem2  23607  xkoptsub  23619  xkopt  23620  xkoco2cn  23623  xkococnlem  23624  xkoinjcn  23652  imasnopn  23655  imasncld  23656  imasncls  23657  qtopkgen  23675  basqtop  23676  tgqtop  23677  qtoprest  23682  kqsat  23696  kqcldsat  23698  kqnrmlem1  23708  kqnrmlem2  23709  hmeontr  23734  reghmph  23758  nrmhmph  23759  fmfnfmlem4  23922  fmfnfm  23923  flimopn  23940  flimclslem  23949  flfnei  23956  lmflf  23970  txflf  23971  fclsopn  23979  fclsfnflim  23992  alexsublem  24009  ptcmplem3  24019  cnextcn  24032  efmndtmd  24066  submtmd  24069  subgtgp  24070  symgtgp  24071  clssubg  24074  clsnsg  24075  tgpconncompeqg  24077  snclseqg  24081  tsmscls  24103  trust  24194  restutop  24202  restutopopn  24203  utop3cls  24216  utopreg  24217  trcfilu  24258  blssec  24400  prdsbl  24456  blssopn  24460  metcnp  24506  cfilucfil  24524  psmetutop  24532  iccntr  24787  icccmplem2  24789  reconnlem1  24792  metnrmlem1a  24824  metnrmlem1  24825  metnrmlem2  24826  metnrmlem3  24827  cnheibor  24922  lebnumlem1  24928  lebnumlem3  24930  lebnumii  24933  clsocv  25217  iscfil2  25233  iscmet3  25260  cmetss  25283  relcmpcmet  25285  bcthlem5  25295  itg1addlem5  25667  perfdvf  25870  dvres3  25880  dvres3a  25881  dvcmul  25911  dvcmulf  25912  dvlip2  25962  lhop1lem  25980  dvcnvrelem1  25984  dvcnvrelem2  25985  dvcnvre  25986  dvcvx  25987  plyco0  26157  plyaddlem1  26178  plymullem1  26179  aalioulem3  26300  ulmdvlem1  26365  precsexlem6  28204  precsexlem7  28205  bdayn0p1  28361  bdaypw2n0bndlem  28455  z12bdaylem2  28463  axcontlem10  29042  eengtrkg  29055  wlkp1lem7  29746  cyclnumvtx  29868  1wlkdlem4  30210  hsupunss  31414  pjpjpre  31490  ssmd2  32383  superpos  32425  atexch  32452  curry2ima  32782  pfxf1  33002  gsumhashmul  33128  symgcom2  33145  pmtrcnelor  33152  cycpmco2lem7  33193  cycpmconjvlem  33202  cycpmconjv  33203  cyc3conja  33218  elrgspnsubrunlem2  33309  subsdrg  33359  nsgmgc  33472  nsgqusf1olem3  33475  elrspunidl  33488  mxidlprm  33530  rprmdvdsprod  33594  dfufd2lem  33609  esplyfvaln  33718  lssdimle  33752  dimkerim  33771  fedgmullem1  33773  fedgmullem2  33774  fedgmul  33775  dimlssid  33776  fldsdrgfldext2  33806  fldextrspunlsplem  33817  fldextrspunlsp  33818  fldextrspunlem1  33819  fldextrspundgdvdslem  33824  fldextrspundgdvds  33825  constr01  33886  constrmon  33888  constrextdg2lem  33892  constrext2chnlem  33894  madjusmdetlem2  33972  zarclsun  34014  rhmpreimacnlem  34028  ordtconnlem1  34068  measiuns  34361  imambfm  34406  cnmbfm  34407  dya2iocnrect  34425  omsfval  34438  omssubaddlem  34443  omssubadd  34444  totprobd  34570  fzssfzo  34683  signstfvn  34713  bnj999  35100  bnj1408  35178  bnj1442  35191  bnj1450  35192  bnj1501  35209  fnrelpredd  35234  revwlk  35307  cvmsss2  35456  cvmliftmolem1  35463  cvmliftlem3  35469  cvmlift2lem9  35493  cvmlift2lem11  35495  cvmlift3lem6  35506  cvmlift3lem7  35507  ssmclslem  35747  mclsax  35751  mclsppslem  35765  mclspps  35766  dfrdg2  35975  neiin  36514  neibastop2  36543  filnetlem4  36563  weiunfrlem  36646  rdgssun  37694  lindsdom  37935  poimirlem11  37952  poimirlem12  37953  itg2addnclem2  37993  cnres2  38084  sstotbnd2  38095  sstotbnd  38096  prdstotbnd  38115  heibor1lem  38130  igenval2  38387  lshpnelb  39430  lcvexchlem4  39483  lsatexch  39489  l1cvat  39501  lkrscss  39544  lkrss  39614  lkreqN  39616  paddunN  40373  osumcllem2N  40403  pmapojoinN  40414  pl42lem2N  40426  dibglbN  41612  diblss  41616  dicvaddcl  41636  dicvscacl  41637  diclss  41639  cdlemn5pre  41646  dihord5apre  41708  dihglblem3N  41741  dihglb2  41788  dochsat  41829  dochshpncl  41830  djhspss  41852  dihsumssj  41854  mapdlsm  42110  hdmaprnlem3eN  42304  hdmaplkr  42359  fnwe2lem2  43479  lnmlsslnm  43509  lmhmfgima  43512  hbtlem6  43557  omabs2  43760  tfsconcatrev  43776  naddwordnexlem0  43824  trrelsuperreldg  44095  iunrelexpuztr  44146  clsk1indlem2  44469  grumnudlem  44712  dvsconst  44757  dvsinax  46341  dvbdfbdioolem1  46356  itgsinexplem1  46382  itgperiod  46409  stoweidlem39  46467  dirkeritg  46530  fourierdlem48  46582  fourierdlem49  46583  fourierdlem70  46604  fourierdlem71  46605  fourierdlem81  46615  issalgend  46766  chnsubseqwl  47309  f1oresf1o  47738  clnbgrgrim  48410  rmsuppss  48846  restcls2lem  49388  iscnrm3rlem7  49421