Theorem eleqtrrd 2836

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eleqtrrd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eleqtrrd.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
eleqtrrd	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrrd

Step	Hyp	Ref	Expression
1		eleqtrrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2739	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrd 2835	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113

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-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-clel 2808

This theorem is referenced by:  3eltr4d  2848  rspc2vd  3895  disjxiun  5092  eldmressnsn  5980  fnsnbg  7107  elimdelov  7451  elovmpt3rab1  7615  fnwelem  8070  tfrlem13  8318  tz7.44-2  8335  omordi  8490  oneo  8505  omeulem2  8507  oeordi  8511  oeeui  8526  nnneo  8579  naddelim  8610  erref  8651  en1uniel  8961  omxpenlem  9001  unblem3  9188  dffi3  9325  ordtypelem10  9423  oismo  9436  cantnff  9574  cantnfp1lem3  9580  cantnflem1  9589  cnfcom  9600  r1ordg  9681  r1pwss  9687  rankwflemb  9696  r1elwf  9699  rankidb  9703  rankonidlem  9731  fseqenlem2  9926  dfac12lem1  10045  dfac12lem2  10046  pwsdompw  10104  ackbij2lem3  10141  ackbij2  10143  cfsmolem  10171  hsmexlem4  10330  ttukeylem3  10412  ttukeylem7  10416  iundom2g  10441  fpwwe2lem8  10539  canthwelem  10551  pwfseqlem4  10563  winalim2  10597  r1wunlim  10638  tskmid  10741  fzopth  13471  predfz  13563  fzoss2  13597  fz1fzo0m1  13620  fzo0addel  13628  fzo0addelr  13629  elfzoext  13632  fzosubel3  13636  elfzomin  13647  elfzonlteqm1  13651  fzoend  13667  fzoopth  13672  fzofzp1  13674  fzofzp1b  13675  peano2fzor  13685  zmodfzo  13808  seqf1olem2  13959  bcn2  14236  swrdccat2  14587  pfxccat1  14619  swrdswrd  14622  pfxccatin12  14650  splfv1  14672  revcl  14678  revlen  14679  revccat  14683  revrev  14684  repswpfx  14702  cshwidxmod  14720  revco  14751  limsupgre  15398  summolem2a  15632  fsumm1  15668  fsumcom2  15691  prodmolem2a  15851  fprodm1  15884  fprodcom2  15901  prmreclem4  16841  prmreclem5  16842  vdwapid1  16897  vdwlem5  16907  vdwlem8  16910  vdwnnlem2  16918  ramub1lem1  16948  ramub1lem2  16949  mrieqvlemd  17545  mreexd  17558  mreexexlemd  17560  catcocl  17601  catass  17602  moni  17653  epii  17660  inviso1  17683  episect  17702  invisoinvl  17707  catsubcat  17756  subccocl  17762  fullsubc  17767  funcco  17788  resf2nd  17812  funcres  17813  fthepi  17847  nati  17875  arwhoma  17962  catccatid  18023  resscatc  18026  catcisolem  18027  catcoppccl  18034  catcfuccl  18035  estrreslem2  18054  funcestrcsetclem3  18058  funcestrcsetclem8  18063  equivestrcsetc  18068  funcsetcestrclem3  18072  funcsetcestrclem8  18078  xpcco  18099  xpcco2  18103  xpccatid  18104  prfcl  18119  catcxpccl  18123  curf12  18143  curf1cl  18144  curf2  18145  curf2cl  18147  curfcl  18148  uncf2  18153  uncfcurf  18155  diag12  18160  diag2  18161  curf2ndf  18163  hofcl  18175  oppchofcl  18176  oyoncl  18186  yonedalem3a  18190  yonedalem4b  18192  yonedalem22  18194  yonedalem3b  18195  yonedalem3  18196  yonedainv  18197  yonffthlem  18198  latcl2  18352  latlem  18353  latjcom  18363  latmcom  18379  clatlem  18418  clatlubcl2  18420  clatglbcl2  18422  acsfiindd  18469  pfxchn  18526  chnind  18537  chnub  18538  chnlt  18539  chnccat  18542  chnrev  18543  gsumpropd2lem  18597  sgrppropd  18649  mndpropd  18677  imasmnd  18693  frmdmnd  18777  frmdgsum  18780  grpsubpropd2  18969  imasgrp  18979  subg0  19055  0ghm  19152  resghm2  19155  ghmco  19158  pwsdiagghm  19166  ghmqusnsglem2  19203  ghmqusnsg  19204  ghmquskerlem2  19207  ghmquskerlem3  19208  ghmqusker  19209  psgnunilem1  19415  psgnunilem5  19416  psgnunilem2  19417  psgnunilem3  19418  sylow1lem4  19523  sylow1lem5  19524  efglem  19638  efgtf  19644  efginvrel2  19649  efginvrel1  19650  efgsdmi  19654  efgs1b  19658  efgsres  19660  efgsfo  19661  efgredleme  19665  efgredlemc  19667  efgredlem  19669  efgcpbllemb  19677  frgp0  19682  frgpadd  19685  frgpinv  19686  vrgpf  19690  vrgpinv  19691  frgpuplem  19694  frgpup1  19697  frgpup2  19698  frgpup3lem  19699  frgpnabllem1  19795  frgpnabllem2  19796  gsumval3  19829  dprdfid  19941  dprdsn  19960  dprd2da  19966  dpjidcl  19982  pgpfac1lem2  19999  pgpfaclem3  20007  ablsimpg1gend  20029  ablsimpgprmd  20039  rngpropd  20102  imasrng  20105  ringpropd  20216  imasring  20258  qusring2  20262  pwsco1rhm  20427  pwsco2rhm  20428  lringuplu  20469  subrgunit  20515  pwsdiagrhm  20532  rnghmsubcsetclem1  20556  zrinitorngc  20567  zrtermorngc  20568  zrzeroorngc  20569  rhmsubcsetclem1  20585  rhmsubcrngclem1  20591  zrtermoringc  20600  zrninitoringc  20601  srhmsubclem2  20603  srhmsubc  20605  cntzsdrg  20727  isabvd  20737  lmodprop2d  20867  islssd  20878  prdsvscacl  20911  prdslmodd  20912  islmhm2  20982  lmhmco  20987  lmhmplusg  20988  lmhmvsca  20989  lmhmpropd  21017  lsppreli  21034  ellspsn4  21071  lssacsex  21091  lspsnat  21092  lidlnsg  21195  qus2idrng  21220  qus1  21221  qusrhm  21223  rhmpreimaidl  21224  rhmqusnsg  21232  rngqiprngghmlem1  21234  rngqiprngfulem1  21258  irinitoringc  21426  nzerooringczr  21427  znf1o  21498  cssmre  21640  dsmmlss  21691  frlmsplit2  21720  frlmbas3  21723  frlmup1  21745  assapropd  21819  psr0cl  21899  psrnegcl  21901  psr1cl  21908  resspsrmul  21923  subrgpsr  21925  mvrf  21932  mplmon  21980  mplcoe1  21982  subrgasclcl  22012  mplind  22015  evlslem1  22027  subrgply1  22155  psrplusgpropd  22158  ply1coe  22223  cply1coe0bi  22227  lply1binomsc  22236  ply1fermltlchr  22237  evls1val  22245  evls1rhm  22247  evl1val  22254  evl1rhm  22257  pf1ind  22280  evl1scvarpw  22288  evls1fpws  22294  mhmcompl  22305  rhmply1  22311  matbas2i  22347  matplusg2  22352  matvsca2  22353  matsubgcell  22359  matvscacell  22361  mpomatmul  22371  mavmulval  22470  mavmulcl  22472  mavmulass  22474  mavmul0  22477  mavmumamul1  22480  m1detdiag  22522  cramerimplem2  22609  mat2pmatmul  22656  mat2pmatlin  22660  monmatcollpw  22704  pmatcollpwfi  22707  mply1topmatcl  22730  pm2mpghm  22741  pm2mpmhmlem2  22744  pm2mp  22750  chpmat1dlem  22760  chpmat1d  22761  chpdmatlem0  22762  chpscmat  22767  chpscmatgsumbin  22769  chpscmatgsummon  22770  chfacfscmulcl  22782  cpmadugsumlemB  22799  cpmadugsumlemC  22800  chcoeffeqlem  22810  cldmreon  23019  neiptopreu  23058  maxlp  23072  ordttopon  23118  ordtrest2lem  23128  cnprcl2  23176  lmcnp  23229  resthauslem  23288  hauscmplem  23331  1stcfb  23370  2ndcctbss  23380  2ndcomap  23383  dis2ndc  23385  loclly  23412  hausllycmp  23419  locfincmp  23451  dissnref  23453  kgeni  23462  kgenidm  23472  ptpjpre2  23505  xkoopn  23514  txopn  23527  ptpjopn  23537  ptcldmpt  23539  ptcls  23541  pthaus  23563  txkgen  23577  xkohaus  23578  xkopt  23580  txconn  23614  imastps  23646  kqid  23653  kqopn  23659  kqcld  23660  isr0  23662  indishmph  23723  pt1hmeo  23731  ptuncnv  23732  ptunhmeo  23733  t0kq  23743  filconn  23808  uzrest  23822  uffixsn  23850  fmfnfmlem2  23880  flimss2  23897  flimss1  23898  flimclslem  23909  flfcnp  23929  fclsfnflim  23952  uffclsflim  23956  fcfelbas  23961  alexsublem  23969  alexsub  23970  cnextcn  23992  cnextfres1  23993  cnextfres  23994  tmdgsum  24020  distgp  24024  indistgp  24025  symgtgp  24031  ghmcnp  24040  qustgpopn  24045  qustgplem  24046  qustgphaus  24048  prdstmdd  24049  prdstgpd  24050  tsmsid  24065  tsmssubm  24068  tsmsmhm  24071  tsmsadd  24072  tsmssplit  24077  utop2nei  24175  utop3cls  24176  neipcfilu  24220  cnextucn  24227  ucnextcn  24228  blpnfctr  24361  lpbl  24428  met2ndci  24447  tmsxps  24461  metcnpi  24469  metcnpi2  24470  metcnpi3  24471  metustid  24479  metustsym  24480  metustexhalf  24481  subgngp  24560  ngptgp  24561  sranlm  24609  nlmvscn  24612  nrginvrcn  24617  lssnlm  24626  nghmcn  24670  iccntr  24747  icccmplem2  24749  msdcn  24767  cncfmptc  24842  cncfmptid  24843  cncfmpt2f  24845  icoopnst  24873  iocopnst  24874  nmoleub2lem3  25052  nmoleub3  25056  nmhmcn  25057  ipcn  25183  cfilfcls  25211  caucfil  25220  equivcau  25237  caubl  25245  flimcfil  25251  cmssmscld  25287  rrxdstprj1  25346  minveclem3b  25365  minveclem4  25369  mulcncf  25383  ovolicc2lem3  25457  ovolicc2lem4  25458  opnmbllem  25539  vitalilem2  25547  mbfsup  25602  mbfinf  25603  mbfi1fseqlem4  25656  limccnp  25829  limccnp2  25830  dvreslem  25847  dvres2lem  25848  dvidlem  25853  dvcnp2  25858  dvcnp2OLD  25859  dvcn  25860  dvaddbr  25877  dvmulbr  25878  dvmulbrOLD  25879  dvcmul  25884  dvcof  25889  dvcnvlem  25917  dvef  25921  rollelem  25930  dvlip2  25937  dvivthlem1  25950  dvivth  25952  lhop2  25957  lhop  25958  dvcnvrelem1  25959  dvcnvrelem2  25960  dvcnvre  25961  ply1rem  26108  fta1blem  26113  plycpn  26234  plyrem  26250  tayl0  26306  dvtaylp  26315  dvntaylp  26316  dvntaylp0  26317  taylthlem1  26318  taylthlem2  26319  taylthlem2OLD  26320  ulmdvlem3  26348  psercn  26373  pserdv  26376  abelth  26388  efabl  26496  efopnlem1  26602  loglesqrt  26708  relogbf  26738  efrlim  26916  efrlimOLD  26917  dchrghm  27204  dchrptlem3  27214  nodenselem5  27637  nosupres  27656  noinfres  27671  sltlpss  27863  precsexlem11  28165  noseq0  28230  noseqp1  28231  noseqrdgfn  28246  noseqrdgsuc  28248  tgbtwntriv2  28475  tgbtwnne  28478  ercgrg  28505  tgidinside  28559  tgbtwnconn1  28563  tglnne  28616  tglnne0  28628  tglnpt2  28629  tglineneq  28632  ncolncol  28634  coltr3  28636  mirln  28664  mirln2  28665  mirconn  28666  krippenlem  28678  footexALT  28706  footexlem1  28707  footexlem2  28708  colperpexlem3  28720  mideulem2  28722  opphllem  28723  oppne3  28731  opphllem1  28735  opphllem2  28736  opphllem4  28738  oppperpex  28741  opphl  28742  hlpasch  28744  hpgerlem  28753  colhp  28758  midbtwn  28767  lmieu  28772  lmiisolem  28784  sacgr  28819  f1otrg  28859  f1otrge  28860  ebtwntg  28971  ecgrtg  28972  eengtrkg  28975  eengtrkge  28976  upgr1eop  29104  usgredg3  29205  uspgr1eop  29236  usgr1eop  29239  vtxdun  29471  vtxdfiun  29472  1loopgruspgr  29490  1loopgrvd2  29493  1hevtxdg1  29496  1egrvtxdg1  29499  1egrvtxdg0  29501  umgr2v2e  29515  wlkres  29658  wlkp1lem4  29664  wlkp1  29669  cyclnumvtx  29789  wwlksm1edg  29870  wwlksnext  29882  wwlksnextproplem3  29900  clwwlkel  30037  1wlkdlem2  30129  trlsegvdeg  30218  eupth2lem3lem1  30219  eupth2lem3lem2  30220  extwwlkfab  30343  numclwlk2lem2f  30368  spansnid  31554  elspansn4  31564  fnpreimac  32664  ccatf1  32941  ccatws1f1olast  32944  swrdrn2  32946  swrdrn3  32947  swrdf1  32948  splfv3  32950  pwrssmgc  32992  wrdpmtrlast  33073  psgnfzto1stlem  33080  cycpmfv1  33093  cycpmfv2  33094  cycpmco2lem2  33107  cycpmco2lem4  33109  cycpmco2lem5  33110  cycpmco2lem6  33111  cycpmco2  33113  cyc3co2  33120  cycpmrn  33123  submarchi  33166  subrdom  33262  fracfld  33285  imaslmod  33329  quslmod  33334  quslmhm  33335  nsgqusf1olem2  33390  lmhmqusker  33393  rhmquskerlem  33401  idlinsubrg  33407  drngidl  33409  rhmpreimaprmidl  33427  qsidomlem2  33429  mxidlprm  33446  opprmxidlabs  33463  qsdrngilem  33470  qsdrngi  33471  qsdrnglem2  33472  idlsrg0g  33482  pidufd  33519  dfufd2lem  33525  fply1  33532  evl1fpws  33538  ressply1evls1  33539  ressply1sub  33544  ply1asclunit  33548  r1plmhm  33581  mplvrpmga  33586  issply  33595  esplympl  33599  drgextlsp  33617  matdim  33639  ply1degltdimlem  33646  lindsunlem  33648  qusdimsum  33652  fedgmullem1  33653  fedgmullem2  33654  fedgmul  33655  extdg1id  33690  evls1fldgencl  33694  irngss  33711  irngnzply1  33715  extdgfialglem1  33716  extdgfialglem2  33717  minplymindeg  33732  minplyirredlem  33734  irredminply  33740  algextdeglem2  33742  constrconj  33769  constrfiss  33775  1smat1  33828  submat1n  33829  lmatfval  33838  lmatcl  33840  mdetpmtr1  33847  madjusmdetlem4  33854  qtopt1  33859  qtophaus  33860  locfinref  33865  zarcls1  33893  zarclsiin  33895  zarmxt1  33904  zarcmplem  33905  rhmpreimacn  33909  ordtrest2NEWlem  33946  elzrhunit  34001  qqhcn  34015  qqhucn  34016  esumel  34071  esumsplit  34077  sigagenss2  34174  elsx  34218  sxbrsigalem0  34295  dya2icoseg  34301  eulerpartlemb  34392  eulerpartlemgvv  34400  iwrdsplit  34411  sseqfv2  34418  probfinmeasb  34452  dstrvprob  34496  dstfrvel  34498  ballotlemrv  34544  signstfvn  34593  signstfvp  34595  signstfveq0  34601  signsvtp  34607  signsvtn  34608  reprsuc  34639  reprpmtf1o  34650  lpadleft  34707  bnj1006  34983  bnj1018g  34986  bnj1018  34987  bnj1121  35008  bnj1398  35057  bnj1450  35073  bnj1501  35090  revpfxsfxrev  35171  swrdrevpfx  35172  pfxwlk  35179  revwlk  35180  swrdwlk  35182  subfacp1lem5  35239  ptpconn  35288  indispconn  35289  cvxsconn  35298  cvmseu  35331  cvmliftmolem2  35337  cvmliftlem7  35346  cvmliftlem10  35349  cvmliftlem13  35351  cvmlift2lem12  35369  satfv1lem  35417  satffunlem1lem2  35458  satffunlem2lem2  35461  satefvfmla1  35480  mrsubcv  35565  mrsubff  35567  mrsubrn  35568  mrsubccat  35573  elmrsubrn  35575  mrsubco  35576  mrsubvrs  35577  mvhf  35613  msubvrs  35615  mclsax  35624  r1peuqusdeg1  35698  linerflx1  36204  linerflx2  36206  fwddifnval  36218  elhf2  36230  neibastop2lem  36415  weiunpo  36520  weiunso  36521  icoreunrn  37414  relowlssretop  37418  sucneqond  37420  matunitlindflem2  37667  poimirlem4  37674  poimirlem20  37690  poimirlem30  37700  broucube  37704  opnmbllem0  37706  areacirclem2  37759  areacirclem4  37761  blssp  37806  sstotbnd2  37824  totbndbnd  37839  prdstotbnd  37844  cnpwstotbnd  37847  heiborlem9  37869  exidcl  37926  exidresid  37929  grpokerinj  37943  iscringd  38048  erimeq2  38786  prter3  38991  toycom  39082  islfld  39171  lshpsmreu  39218  ldualelvbase  39236  ldualssvscl  39267  lkreqN  39279  lkrlspeqN  39280  erng1lem  41096  erngdvlem4  41100  erng0g  41103  erng1r  41104  erngdvlem4-rN  41108  dva0g  41136  dia1dim2  41171  dia1dimid  41172  dia2dimlem5  41177  dvhelvbasei  41197  dvhvaddass  41206  tendoinvcl  41213  tendolinv  41214  tendorinv  41215  dvhgrp  41216  dvhlveclem  41217  cdlemn4  41307  lcfrlem12N  41663  lcfrlem15  41666  lcdvscl  41714  lcdlssvscl  41715  lcdvsass  41716  lcdvs0N  41725  mapdincl  41770  mapdin  41771  mapdlsmcl  41772  mapdcnvatN  41775  mapdpglem2  41782  mapdpglem12  41792  mapdpglem18  41798  mapdpglem21  41801  mapdpglem22  41802  mapdpglem28  41810  mapdpglem30  41811  hdmaprnlem3N  41959  hdmaprnlem3uN  41960  hdmaprnlem7N  41964  hdmaprnlem8N  41965  hdmaprnlem9N  41966  hdmaprnlem3eN  41967  hdmaprnlem16N  41971  hgmapdcl  41999  hgmapval1  42002  hgmaprnlem4N  42008  hdmapinvlem1  42027  fzadd2d  42081  aks6d1c2lem4  42230  sticksstones1  42249  sticksstones8  42256  sticksstones9  42257  sticksstones10  42258  sticksstones11  42259  sticksstones17  42266  sticksstones18  42267  aks6d1c6lem4  42276  rhmqusspan  42288  aks5lem2  42290  mhmcopsr  42657  evlsbagval  42674  evlsevl  42679  evlvvval  42681  evlvvvallem  42682  selvcllem2  42686  evlselv  42695  mhpind  42702  fltnltalem  42770  wepwsolem  43149  kercvrlsm  43190  dfacbasgrp  43215  onexomgt  43348  onexoegt  43351  onov0suclim  43381  cantnftermord  43427  cantnf2  43432  omcl2  43440  ofoaf  43462  ofoafo  43463  grurankcld  44340  grumnudlem  44392  grumnud  44393  inaex  44404  gruex  44405  dvconstbi  44441  cncmpmax  45143  iooabslt  45613  fmul01lt1lem2  45699  limciccioolb  45735  limcicciooub  45749  limsuppnfdlem  45813  climrescn  45860  climxrrelem  45861  climxrre  45862  liminflimsupxrre  45929  xlimmnfvlem2  45945  xlimpnfvlem2  45949  fsumcncf  45990  ioccncflimc  45997  icocncflimc  46001  cncfiooicclem1  46005  dvbdfbdioolem2  46041  dvnmul  46055  dvnprodlem1  46058  stoweidlem26  46138  stoweidlem34  46146  stoweidlem48  46160  stoweidlem59  46171  dirkercncflem3  46217  fourierdlem32  46251  fourierdlem41  46260  fourierdlem51  46269  fourierdlem63  46281  fourierdlem82  46300  fourierdlem85  46303  fourierdlem93  46311  fourierdlem111  46329  fourierdlem114  46332  etransclem35  46381  hspdifhsp  46728  opnvonmbllem1  46744  ovnovollem1  46768  mbfresmf  46851  smfaddlem1  46875  smfsuplem1  46923  smflimsuplem5  46936  chnerlem2  46995  setsidel  47490  setsnidel  47491  imasetpreimafvbijlemf  47515  prelspr  47600  upgrimpths  48023  gpgprismgr4cycllem9  48217  rngccatidALTV  48386  rhmsubcALTVlem3  48397  funcringcsetcALTV2lem3  48406  funcringcsetcALTV2lem8  48411  ringccatidALTV  48420  funcringcsetclem3ALTV  48429  funcringcsetclem8ALTV  48434  srhmsubcALTVlem1  48437  srhmsubcALTV  48439  lcosslsp  48553  nnolog2flm1  48705  ffvbr  48970  glbprlem  49079  topdlat  49118  catprs  49126  iinfsubc  49173  iinfconstbaslem  49180  imaid  49269  fthcomf  49272  uptr2  49336  natoppf2  49345  natoppfb  49346  swapf2  49389  swapfiso  49400  swapciso  49401  oppc1stflem  49402  cofuswapf2  49410  fuco22natlem  49460  fucoppcffth  49526  oppcthinco  49554  oppcthinendcALT  49556  thinccisod  49569  termco  49596  termchommo  49600  termcid  49601  termcterm  49628  termcterm2  49629  diagciso  49654  diagcic  49655  funcsn  49656  uobeqterm  49661  mndtccatid  49702  grptcmon  49708  grptcepi  49709  2arwcat  49715  lanval2  49742  ranval2  49745  lanup  49756  ranup  49757  lmddu  49782