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

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

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 2123  ax-ext 2708

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

This theorem is referenced by:  3sstr4d  3989  fssrescdmd  7071  funfvima2d  7178  fnfvima  7179  frrlem8  8235  frrlem10  8237  fprresex  8252  oaordi  8473  omordi  8493  omlimcl  8505  oen0  8514  domunsncan  9005  f1opwfi  9256  cantnfle  9580  cantnflt  9581  cantnflem1d  9597  ttrcltr  9625  r1pwss  9696  rankxplim3  9793  acndom2  9964  fodomfi2  9970  cflm  10160  cflim2  10173  isf34lem5  10288  isf34lem7  10289  isf34lem6  10290  axdc2lem  10358  ttukeylem5  10423  wunex2  10649  ssfzunsn  13486  ccatass  14512  swrdval2  14570  splfv2a  14679  revccat  14689  cshimadifsn  14752  cshimadifsn0  14753  rtrclreclem1  14980  rtrclreclem2  14982  sumrblem  15634  prodrblem  15852  dfphi2  16701  vdwlem1  16909  basprssdmsets  17148  imasaddfnlem  17449  imasaddvallem  17450  imasvscafn  17458  imasvscaval  17459  mreexexlem4d  17570  mreexfidimd  17573  sscpwex  17739  acsmap2d  18478  gsumress  18607  subsubmgm  18635  subsubm  18741  frmdsssubm  18786  frmdss2  18788  subsubg  19079  cntzmhm2  19271  cntzcmnf  19774  ablcntzd  19786  gsumzsubmcl  19847  gsumconst  19863  gsumzmhm  19866  subgdmdprd  19965  dprdcntz2  19969  dprd2da  19973  dmdprdsplit2lem  19976  ablfac1eu  20004  pgpfaclem1  20012  pgpfaclem2  20013  subsubrng  20496  subsubrg  20531  issubdrg  20713  subdrgint  20736  lmhmlsp  21001  lspsntri  21049  lspindpi  21087  lidldvgen  21289  gsumfsum  21389  mrccss  21649  frlmsslsp  21751  opsrtoslem2  22011  ressply1evl  22314  scmatsgrp1  22466  toponss  22871  ssntr  23002  elcls3  23027  toponmre  23037  neiptoptop  23075  neiptopnei  23076  neitr  23124  ordtbas  23136  ordtopn1  23138  ordtopn2  23139  iscnp3  23188  tgcn  23196  tgcnp  23197  ssidcn  23199  cnclsi  23216  cncls  23218  cncnp  23224  lmcld  23247  tgcmp  23345  cnconn  23366  connima  23369  clsconn  23374  conncompcld  23378  1stccnp  23406  kgentopon  23482  llycmpkgen2  23494  1stckgen  23498  kgencn2  23501  ptopn  23527  txcls  23548  ptpjcn  23555  ptclsg  23559  xkoccn  23563  txcnp  23564  ptcnplem  23565  txcmplem2  23586  xkoptsub  23598  xkopt  23599  xkoco2cn  23602  xkococnlem  23603  xkoinjcn  23631  imasnopn  23634  imasncld  23635  imasncls  23636  qtopkgen  23654  basqtop  23655  tgqtop  23656  qtoprest  23661  kqsat  23675  kqcldsat  23677  kqnrmlem1  23687  kqnrmlem2  23688  hmeontr  23713  reghmph  23737  nrmhmph  23738  fmfnfmlem4  23901  fmfnfm  23902  flimopn  23919  flimclslem  23928  flfnei  23935  lmflf  23949  txflf  23950  fclsopn  23958  fclsfnflim  23971  alexsublem  23988  ptcmplem3  23998  cnextcn  24011  efmndtmd  24045  submtmd  24048  subgtgp  24049  symgtgp  24050  clssubg  24053  clsnsg  24054  tgpconncompeqg  24056  snclseqg  24060  tsmscls  24082  trust  24173  restutop  24181  restutopopn  24182  utop3cls  24195  utopreg  24196  trcfilu  24237  blssec  24379  prdsbl  24435  blssopn  24439  metcnp  24485  cfilucfil  24503  psmetutop  24511  iccntr  24766  icccmplem2  24768  reconnlem1  24771  metnrmlem1a  24803  metnrmlem1  24804  metnrmlem2  24805  metnrmlem3  24806  cnheibor  24910  lebnumlem1  24916  lebnumlem3  24918  lebnumii  24921  clsocv  25206  iscfil2  25222  iscmet3  25249  cmetss  25272  relcmpcmet  25274  bcthlem5  25284  itg1addlem5  25657  perfdvf  25860  dvres3  25870  dvres3a  25871  dvcmul  25903  dvcmulf  25904  dvlip2  25956  lhop1lem  25974  dvcnvrelem1  25978  dvcnvrelem2  25979  dvcnvre  25980  dvcvx  25981  plyco0  26153  plyaddlem1  26174  plymullem1  26175  aalioulem3  26298  ulmdvlem1  26365  precsexlem6  28208  precsexlem7  28209  bdayn0p1  28365  bdaypw2n0bndlem  28459  z12bdaylem2  28467  axcontlem10  29046  eengtrkg  29059  wlkp1lem7  29751  cyclnumvtx  29873  1wlkdlem4  30215  hsupunss  31418  pjpjpre  31494  ssmd2  32387  superpos  32429  atexch  32456  curry2ima  32788  pfxf1  33024  gsumhashmul  33150  symgcom2  33166  pmtrcnelor  33173  cycpmco2lem7  33214  cycpmconjvlem  33223  cycpmconjv  33224  cyc3conja  33239  elrgspnsubrunlem2  33330  subsdrg  33380  nsgmgc  33493  nsgqusf1olem3  33496  elrspunidl  33509  mxidlprm  33551  rprmdvdsprod  33615  dfufd2lem  33630  lssdimle  33764  dimkerim  33784  fedgmullem1  33786  fedgmullem2  33787  fedgmul  33788  dimlssid  33789  fldsdrgfldext2  33819  fldextrspunlsplem  33830  fldextrspunlsp  33831  fldextrspunlem1  33832  fldextrspundgdvdslem  33837  fldextrspundgdvds  33838  constr01  33899  constrmon  33901  constrextdg2lem  33905  constrext2chnlem  33907  madjusmdetlem2  33985  zarclsun  34027  rhmpreimacnlem  34041  ordtconnlem1  34081  measiuns  34374  imambfm  34419  cnmbfm  34420  dya2iocnrect  34438  omsfval  34451  omssubaddlem  34456  omssubadd  34457  totprobd  34583  fzssfzo  34696  signstfvn  34726  bnj999  35114  bnj1408  35192  bnj1442  35205  bnj1450  35206  bnj1501  35223  fnrelpredd  35247  revwlk  35319  cvmsss2  35468  cvmliftmolem1  35475  cvmliftlem3  35481  cvmlift2lem9  35505  cvmlift2lem11  35507  cvmlift3lem6  35518  cvmlift3lem7  35519  ssmclslem  35759  mclsax  35763  mclsppslem  35777  mclspps  35778  dfrdg2  35987  neiin  36526  neibastop2  36555  filnetlem4  36575  weiunfrlem  36658  rdgssun  37579  lindsdom  37811  poimirlem11  37828  poimirlem12  37829  itg2addnclem2  37869  cnres2  37960  sstotbnd2  37971  sstotbnd  37972  prdstotbnd  37991  heibor1lem  38006  igenval2  38263  lshpnelb  39240  lcvexchlem4  39293  lsatexch  39299  l1cvat  39311  lkrscss  39354  lkrss  39424  lkreqN  39426  paddunN  40183  osumcllem2N  40213  pmapojoinN  40224  pl42lem2N  40236  dibglbN  41422  diblss  41426  dicvaddcl  41446  dicvscacl  41447  diclss  41449  cdlemn5pre  41456  dihord5apre  41518  dihglblem3N  41551  dihglb2  41598  dochsat  41639  dochshpncl  41640  djhspss  41662  dihsumssj  41664  mapdlsm  41920  hdmaprnlem3eN  42114  hdmaplkr  42169  fnwe2lem2  43289  lnmlsslnm  43319  lmhmfgima  43322  hbtlem6  43367  omabs2  43570  tfsconcatrev  43586  naddwordnexlem0  43634  trrelsuperreldg  43905  iunrelexpuztr  43956  clsk1indlem2  44279  grumnudlem  44522  dvsconst  44567  dvsinax  46153  dvbdfbdioolem1  46168  itgsinexplem1  46194  itgperiod  46221  stoweidlem39  46279  dirkeritg  46342  fourierdlem48  46394  fourierdlem49  46395  fourierdlem70  46416  fourierdlem71  46417  fourierdlem81  46427  issalgend  46578  chnsubseqwl  47119  f1oresf1o  47532  clnbgrgrim  48176  rmsuppss  48612  restcls2lem  49154  iscnrm3rlem7  49187