Theorem sseqtrrd 3977

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

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

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 2156  ax-ext 2738

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

This theorem is used by:  3sstr4d  3995  fssrescdmd  7129  funfvima2d  7237  fnfvima  7238  frrlem8  8299  frrlem10  8301  fprresex  8316  oaordi  8540  omordi  8560  omlimcl  8572  oen0  8581  domunsncan  9075  f1opwfi  9323  cantnfle  9650  cantnflt  9651  cantnflem1d  9667  ttrcltr  9695  r1pwss  9766  rankxplim3  9863  acndom2  10057  fodomfi2  10063  cflm  10251  cflim2  10265  isf34lem5  10380  isf34lem7  10381  isf34lem6  10382  axdc2lem  10450  ttukeylem5  10515  wunex2  10741  ssfzunsn  13617  ccatass  14646  swrdval2  14706  splfv2a  14817  revccat  14827  cshimadifsn  14892  cshimadifsn0  14893  rtrclreclem1  15120  rtrclreclem2  15122  sumrblem  15788  prodrblem  16009  dfphi2  16858  vdwlem1  17066  basprssdmsets  17306  imasaddfnlem  17607  imasaddvallem  17608  imasvscafn  17616  imasvscaval  17617  mreexexlem4d  17728  mreexfidimd  17731  sscpwex  17897  acsmap2d  18636  gsumress  18769  subsubmgm  18797  subsubm  18906  frmdsssubm  18951  frmdss2  18953  subsubg  19247  cntzmhm2  19443  cntzcmnf  19946  ablcntzd  19958  gsumzsubmcl  20019  gsumconst  20035  gsumzmhm  20038  subgdmdprd  20137  dprdcntz2  20141  dprd2da  20145  dmdprdsplit2lem  20148  ablfac1eu  20176  pgpfaclem1  20184  pgpfaclem2  20185  subsubrng  20699  subsubrg  20734  issubdrg  20920  subdrgint  20943  lmhmlsp  21207  lspsntri  21255  lspindpi  21293  rspprop  21407  lidldvgen  21539  gsumfsum  21621  mrccss  21881  frlmsslsp  21983  opsrtoslem2  22244  ressply1evl  22567  scmatsgrp1  22716  toponss  23121  ssntr  23252  elcls3  23277  toponmre  23287  neiptoptop  23325  neiptopnei  23326  neitr  23374  ordtbas  23386  ordtopn1  23388  ordtopn2  23389  iscnp3  23438  tgcn  23446  tgcnp  23447  ssidcn  23449  cnclsi  23466  cncls  23468  cncnp  23474  lmcld  23497  tgcmp  23595  cnconn  23616  connima  23619  clsconn  23624  conncompcld  23628  1stccnp  23656  kgentopon  23732  llycmpkgen2  23744  1stckgen  23748  kgencn2  23751  ptopn  23777  txcls  23798  ptpjcn  23805  ptclsg  23809  xkoccn  23813  txcnp  23814  ptcnplem  23815  txcmplem2  23836  xkoptsub  23848  xkopt  23849  xkoco2cn  23852  xkococnlem  23853  xkoinjcn  23881  imasnopn  23884  imasncld  23885  imasncls  23886  qtopkgen  23904  basqtop  23905  tgqtop  23906  qtoprest  23911  kqsat  23925  kqcldsat  23927  kqnrmlem1  23937  kqnrmlem2  23938  hmeontr  23963  reghmph  23987  nrmhmph  23988  fmfnfmlem4  24151  fmfnfm  24152  flimopn  24169  flimclslem  24178  flfnei  24185  lmflf  24199  txflf  24200  fclsopn  24208  fclsfnflim  24221  alexsublem  24238  ptcmplem3  24248  cnextcn  24261  efmndtmd  24295  submtmd  24298  subgtgp  24299  symgtgp  24300  clssubg  24303  clsnsg  24304  tgpconncompeqg  24306  snclseqg  24310  tsmscls  24332  trust  24423  restutop  24431  restutopopn  24432  utop3cls  24445  utopreg  24446  trcfilu  24487  blssec  24629  prdsbl  24685  blssopn  24689  metcnp  24735  cfilucfil  24753  psmetutop  24761  iccntr  25016  icccmplem2  25018  reconnlem1  25021  metnrmlem1a  25053  metnrmlem1  25054  metnrmlem2  25055  metnrmlem3  25056  cnheibor  25151  lebnumlem1  25157  lebnumlem3  25159  lebnumii  25162  clsocv  25446  iscfil2  25462  iscmet3  25489  cmetss  25512  relcmpcmet  25514  bcthlem5  25524  itg1addlem5  25896  perfdvf  26099  dvres3  26109  dvres3a  26110  dvcmul  26140  dvcmulf  26141  dvlip2  26191  lhop1lem  26209  dvcnvrelem1  26213  dvcnvrelem2  26214  dvcnvre  26215  dvcvx  26216  plyco0  26386  plyaddlem1  26407  plymullem1  26408  aalioulem3  26534  ulmdvlem1  26600  precsexlem6  28442  precsexlem7  28443  bdayn0p1  28599  bdaypw2n0bndlem  28693  z12bdaylem2  28701  plngrotlem1  29106  lnssplnglem  29110  prlngpln4  29245  quadcgrprlng  29253  axcontlem10  29360  eengtrkg  29373  wlkp1lem7  30064  cyclnumvtx  30186  1wlkdlem4  30528  hsupunss  31732  pjpjpre  31808  ssmd2  32701  superpos  32743  atexch  32770  curry2ima  33091  pfxf1  33299  gsumhashmul  33418  symgcom2  33435  pmtrcnelor  33442  cycpmco2lem7  33483  cycpmconjvlem  33492  cycpmconjv  33493  cyc3conja  33508  elrgspnsubrunlem2  33599  subsdrg  33650  nsgmgc  33752  nsgqusf1olem3  33755  elrspunidl  33767  mxidlprm  33784  rprmdvdsprod  33855  dfufd2lem  33870  esplyfvaln  33995  lssdimle  34029  dimkerim  34048  fedgmullem1  34050  fedgmullem2  34051  fedgmul  34052  dimlssid  34053  fldsdrgfldext2  34083  fldextrspunlsplem  34094  fldextrspunlsp  34095  fldextrspunlem1  34096  fldextrspundgdvdslem  34101  fldextrspundgdvds  34102  constr01  34163  constrmon  34165  constrextdg2lem  34169  constrext2chnlem  34171  madjusmdetlem2  34249  zarclsun  34291  rhmpreimacnlem  34305  ordtconnlem1  34345  measiuns  34638  imambfm  34683  cnmbfm  34684  dya2iocnrect  34702  omsfval  34715  omssubaddlem  34720  omssubadd  34721  totprobd  34847  fzssfzo  34960  signstfvn  34987  bnj999  35377  bnj1408  35455  bnj1442  35468  bnj1450  35469  bnj1501  35486  fnrelpredd  35506  revwlk  35637  cvmsss2  35786  cvmliftmolem1  35793  cvmliftlem3  35799  cvmlift2lem9  35823  cvmlift2lem11  35825  cvmlift3lem6  35836  cvmlift3lem7  35837  ssmclslem  36077  mclsax  36081  mclsppslem  36095  mclspps  36096  dfrdg2  36305  neiin  36883  neibastop2  36912  filnetlem4  36932  weiunfrlem  37015  rdgssun  38064  lindsdom  38305  poimirlem11  38322  poimirlem12  38323  itg2addnclem2  38363  cnres2  38454  sstotbnd2  38465  sstotbnd  38466  prdstotbnd  38485  heibor1lem  38500  igenval2  38757  lshpnelb  39798  lcvexchlem4  39851  lsatexch  39857  l1cvat  39869  lkrscss  39912  lkrss  39982  lkreqN  39984  paddunN  40741  osumcllem2N  40771  pmapojoinN  40782  pl42lem2N  40794  dibglbN  41980  diblss  41984  dicvaddcl  42004  dicvscacl  42005  diclss  42007  cdlemn5pre  42014  dihord5apre  42076  dihglblem3N  42109  dihglb2  42156  dochsat  42197  dochshpncl  42198  djhspss  42220  dihsumssj  42222  mapdlsm  42478  hdmaprnlem3eN  42672  hdmaplkr  42727  fnwe2lem2  43818  lnmlsslnm  43848  lmhmfgima  43851  hbtlem6  43896  omabs2  44099  tfsconcatrev  44115  naddwordnexlem0  44163  trrelsuperreldg  44434  iunrelexpuztr  44485  clsk1indlem2  44808  grumnudlem  45035  dvsconst  45080  dvsinax  46667  dvbdfbdioolem1  46682  itgsinexplem1  46708  itgperiod  46735  stoweidlem39  46793  dirkeritg  46856  fourierdlem48  46908  fourierdlem49  46909  fourierdlem70  46930  fourierdlem71  46931  fourierdlem81  46941  issalgend  47092  chnsubseqwl  47635  f1oresf1o  48067  clnbgrgrim  48739  rmsuppss  49190  restcls2lem  49731  iscnrm3rlem7  49764