Theorem eleqtrrd 2840

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 2743	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrd 2839	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

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-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  3eltr4d  2852  rspc2vd  3899  disjxiun  5097  eldmressnsn  5993  fnsnbg  7122  elimdelov  7466  elovmpt3rab1  7630  fnwelem  8085  tfrlem13  8333  tz7.44-2  8350  omordi  8505  oneo  8520  omeulem2  8522  oeordi  8527  oeeui  8542  nnneo  8595  naddelim  8626  erref  8668  en1uniel  8980  omxpenlem  9020  unblem3  9208  dffi3  9348  ordtypelem10  9446  oismo  9459  cantnff  9597  cantnfp1lem3  9603  cantnflem1  9612  cnfcom  9623  r1ordg  9704  r1pwss  9710  rankwflemb  9719  r1elwf  9722  rankidb  9726  rankonidlem  9754  fseqenlem2  9949  dfac12lem1  10068  dfac12lem2  10069  pwsdompw  10127  ackbij2lem3  10164  ackbij2  10166  cfsmolem  10194  hsmexlem4  10353  ttukeylem3  10435  ttukeylem7  10439  iundom2g  10464  fpwwe2lem8  10563  canthwelem  10575  pwfseqlem4  10587  winalim2  10621  r1wunlim  10662  tskmid  10765  fzopth  13491  predfz  13583  fzoss2  13617  fz1fzo0m1  13640  fzo0addel  13648  fzo0addelr  13649  elfzoext  13652  fzosubel3  13656  elfzomin  13667  elfzonlteqm1  13671  fzoend  13687  fzoopth  13692  fzofzp1  13694  fzofzp1b  13695  peano2fzor  13705  zmodfzo  13828  seqf1olem2  13979  bcn2  14256  swrdccat2  14607  pfxccat1  14639  swrdswrd  14642  pfxccatin12  14670  splfv1  14692  revcl  14698  revlen  14699  revccat  14703  revrev  14704  repswpfx  14722  cshwidxmod  14740  revco  14771  limsupgre  15418  summolem2a  15652  fsumm1  15688  fsumcom2  15711  prodmolem2a  15871  fprodm1  15904  fprodcom2  15921  prmreclem4  16861  prmreclem5  16862  vdwapid1  16917  vdwlem5  16927  vdwlem8  16930  vdwnnlem2  16938  ramub1lem1  16968  ramub1lem2  16969  mrieqvlemd  17566  mreexd  17579  mreexexlemd  17581  catcocl  17622  catass  17623  moni  17674  epii  17681  inviso1  17704  episect  17723  invisoinvl  17728  catsubcat  17777  subccocl  17783  fullsubc  17788  funcco  17809  resf2nd  17833  funcres  17834  fthepi  17868  nati  17896  arwhoma  17983  catccatid  18044  resscatc  18047  catcisolem  18048  catcoppccl  18055  catcfuccl  18056  estrreslem2  18075  funcestrcsetclem3  18079  funcestrcsetclem8  18084  equivestrcsetc  18089  funcsetcestrclem3  18093  funcsetcestrclem8  18099  xpcco  18120  xpcco2  18124  xpccatid  18125  prfcl  18140  catcxpccl  18144  curf12  18164  curf1cl  18165  curf2  18166  curf2cl  18168  curfcl  18169  uncf2  18174  uncfcurf  18176  diag12  18181  diag2  18182  curf2ndf  18184  hofcl  18196  oppchofcl  18197  oyoncl  18207  yonedalem3a  18211  yonedalem4b  18213  yonedalem22  18215  yonedalem3b  18216  yonedalem3  18217  yonedainv  18218  yonffthlem  18219  latcl2  18373  latlem  18374  latjcom  18384  latmcom  18400  clatlem  18439  clatlubcl2  18441  clatglbcl2  18443  acsfiindd  18490  pfxchn  18547  chnind  18558  chnub  18559  chnlt  18560  chnccat  18563  chnrev  18564  gsumpropd2lem  18618  sgrppropd  18670  mndpropd  18698  imasmnd  18714  frmdmnd  18798  frmdgsum  18801  grpsubpropd2  18993  imasgrp  19003  subg0  19079  0ghm  19176  resghm2  19179  ghmco  19182  pwsdiagghm  19190  ghmqusnsglem2  19227  ghmqusnsg  19228  ghmquskerlem2  19231  ghmquskerlem3  19232  ghmqusker  19233  psgnunilem1  19439  psgnunilem5  19440  psgnunilem2  19441  psgnunilem3  19442  sylow1lem4  19547  sylow1lem5  19548  efglem  19662  efgtf  19668  efginvrel2  19673  efginvrel1  19674  efgsdmi  19678  efgs1b  19682  efgsres  19684  efgsfo  19685  efgredleme  19689  efgredlemc  19691  efgredlem  19693  efgcpbllemb  19701  frgp0  19706  frgpadd  19709  frgpinv  19710  vrgpf  19714  vrgpinv  19715  frgpuplem  19718  frgpup1  19721  frgpup2  19722  frgpup3lem  19723  frgpnabllem1  19819  frgpnabllem2  19820  gsumval3  19853  dprdfid  19965  dprdsn  19984  dprd2da  19990  dpjidcl  20006  pgpfac1lem2  20023  pgpfaclem3  20031  ablsimpg1gend  20053  ablsimpgprmd  20063  rngpropd  20126  imasrng  20129  ringpropd  20240  imasring  20283  qusring2  20287  pwsco1rhm  20452  pwsco2rhm  20453  lringuplu  20494  subrgunit  20540  pwsdiagrhm  20557  rnghmsubcsetclem1  20581  zrinitorngc  20592  zrtermorngc  20593  zrzeroorngc  20594  rhmsubcsetclem1  20610  rhmsubcrngclem1  20616  zrtermoringc  20625  zrninitoringc  20626  srhmsubclem2  20628  srhmsubc  20630  cntzsdrg  20752  isabvd  20762  lmodprop2d  20892  islssd  20903  prdsvscacl  20936  prdslmodd  20937  islmhm2  21007  lmhmco  21012  lmhmplusg  21013  lmhmvsca  21014  lmhmpropd  21042  lsppreli  21059  ellspsn4  21096  lssacsex  21116  lspsnat  21117  lidlnsg  21220  qus2idrng  21245  qus1  21246  qusrhm  21248  rhmpreimaidl  21249  rhmqusnsg  21257  rngqiprngghmlem1  21259  rngqiprngfulem1  21283  irinitoringc  21451  nzerooringczr  21452  znf1o  21523  cssmre  21665  dsmmlss  21716  frlmsplit2  21745  frlmbas3  21748  frlmup1  21770  assapropd  21844  psr0cl  21925  psrnegcl  21927  psr1cl  21933  resspsrmul  21948  subrgpsr  21950  mvrf  21957  mplmon  22007  mplcoe1  22009  subrgasclcl  22039  mplind  22042  evlslem1  22054  subrgply1  22190  psrplusgpropd  22193  ply1coe  22259  cply1coe0bi  22263  lply1binomsc  22272  ply1fermltlchr  22273  evls1val  22281  evls1rhm  22283  evl1val  22290  evl1rhm  22293  pf1ind  22316  evl1scvarpw  22324  evls1fpws  22330  mhmcompl  22341  rhmply1  22347  matbas2i  22383  matplusg2  22388  matvsca2  22389  matsubgcell  22395  matvscacell  22397  mpomatmul  22407  mavmulval  22506  mavmulcl  22508  mavmulass  22510  mavmul0  22513  mavmumamul1  22516  m1detdiag  22558  cramerimplem2  22645  mat2pmatmul  22692  mat2pmatlin  22696  monmatcollpw  22740  pmatcollpwfi  22743  mply1topmatcl  22766  pm2mpghm  22777  pm2mpmhmlem2  22780  pm2mp  22786  chpmat1dlem  22796  chpmat1d  22797  chpdmatlem0  22798  chpscmat  22803  chpscmatgsumbin  22805  chpscmatgsummon  22806  chfacfscmulcl  22818  cpmadugsumlemB  22835  cpmadugsumlemC  22836  chcoeffeqlem  22846  cldmreon  23055  neiptopreu  23094  maxlp  23108  ordttopon  23154  ordtrest2lem  23164  cnprcl2  23212  lmcnp  23265  resthauslem  23324  hauscmplem  23367  1stcfb  23406  2ndcctbss  23416  2ndcomap  23419  dis2ndc  23421  loclly  23448  hausllycmp  23455  locfincmp  23487  dissnref  23489  kgeni  23498  kgenidm  23508  ptpjpre2  23541  xkoopn  23550  txopn  23563  ptpjopn  23573  ptcldmpt  23575  ptcls  23577  pthaus  23599  txkgen  23613  xkohaus  23614  xkopt  23616  txconn  23650  imastps  23682  kqid  23689  kqopn  23695  kqcld  23696  isr0  23698  indishmph  23759  pt1hmeo  23767  ptuncnv  23768  ptunhmeo  23769  t0kq  23779  filconn  23844  uzrest  23858  uffixsn  23886  fmfnfmlem2  23916  flimss2  23933  flimss1  23934  flimclslem  23945  flfcnp  23965  fclsfnflim  23988  uffclsflim  23992  fcfelbas  23997  alexsublem  24005  alexsub  24006  cnextcn  24028  cnextfres1  24029  cnextfres  24030  tmdgsum  24056  distgp  24060  indistgp  24061  symgtgp  24067  ghmcnp  24076  qustgpopn  24081  qustgplem  24082  qustgphaus  24084  prdstmdd  24085  prdstgpd  24086  tsmsid  24101  tsmssubm  24104  tsmsmhm  24107  tsmsadd  24108  tsmssplit  24113  utop2nei  24211  utop3cls  24212  neipcfilu  24256  cnextucn  24263  ucnextcn  24264  blpnfctr  24397  lpbl  24464  met2ndci  24483  tmsxps  24497  metcnpi  24505  metcnpi2  24506  metcnpi3  24507  metustid  24515  metustsym  24516  metustexhalf  24517  subgngp  24596  ngptgp  24597  sranlm  24645  nlmvscn  24648  nrginvrcn  24653  lssnlm  24662  nghmcn  24706  iccntr  24783  icccmplem2  24785  msdcn  24803  cncfmptc  24878  cncfmptid  24879  cncfmpt2f  24881  icoopnst  24909  iocopnst  24910  nmoleub2lem3  25088  nmoleub3  25092  nmhmcn  25093  ipcn  25219  cfilfcls  25247  caucfil  25256  equivcau  25273  caubl  25281  flimcfil  25287  cmssmscld  25323  rrxdstprj1  25382  minveclem3b  25401  minveclem4  25405  mulcncf  25419  ovolicc2lem3  25493  ovolicc2lem4  25494  opnmbllem  25575  vitalilem2  25583  mbfsup  25638  mbfinf  25639  mbfi1fseqlem4  25692  limccnp  25865  limccnp2  25866  dvreslem  25883  dvres2lem  25884  dvidlem  25889  dvcnp2  25894  dvcnp2OLD  25895  dvcn  25896  dvaddbr  25913  dvmulbr  25914  dvmulbrOLD  25915  dvcmul  25920  dvcof  25925  dvcnvlem  25953  dvef  25957  rollelem  25966  dvlip2  25973  dvivthlem1  25986  dvivth  25988  lhop2  25993  lhop  25994  dvcnvrelem1  25995  dvcnvrelem2  25996  dvcnvre  25997  ply1rem  26144  fta1blem  26149  plycpn  26270  plyrem  26286  tayl0  26342  dvtaylp  26351  dvntaylp  26352  dvntaylp0  26353  taylthlem1  26354  taylthlem2  26355  taylthlem2OLD  26356  ulmdvlem3  26384  psercn  26409  pserdv  26412  abelth  26424  efabl  26532  efopnlem1  26638  loglesqrt  26744  relogbf  26774  efrlim  26952  efrlimOLD  26953  dchrghm  27240  dchrptlem3  27250  nodenselem5  27673  nosupres  27692  noinfres  27707  ltslpss  27921  precsexlem11  28230  noseq0  28303  noseqp1  28304  noseqrdgfn  28319  noseqrdgsuc  28321  tgbtwntriv2  28577  tgbtwnne  28580  ercgrg  28607  tgidinside  28661  tgbtwnconn1  28665  tglnne  28718  tglnne0  28730  tglnpt2  28731  tglineneq  28734  ncolncol  28736  coltr3  28738  mirln  28766  mirln2  28767  mirconn  28768  krippenlem  28780  footexALT  28808  footexlem1  28809  footexlem2  28810  colperpexlem3  28822  mideulem2  28824  opphllem  28825  oppne3  28833  opphllem1  28837  opphllem2  28838  opphllem4  28840  oppperpex  28843  opphl  28844  hlpasch  28846  hpgerlem  28855  colhp  28860  midbtwn  28869  lmieu  28874  lmiisolem  28886  sacgr  28921  f1otrg  28961  f1otrge  28962  ebtwntg  29073  ecgrtg  29074  eengtrkg  29077  eengtrkge  29078  upgr1eop  29206  usgredg3  29307  uspgr1eop  29338  usgr1eop  29341  vtxdun  29573  vtxdfiun  29574  1loopgruspgr  29592  1loopgrvd2  29595  1hevtxdg1  29598  1egrvtxdg1  29601  1egrvtxdg0  29603  umgr2v2e  29617  wlkres  29760  wlkp1lem4  29766  wlkp1  29771  cyclnumvtx  29891  wwlksm1edg  29972  wwlksnext  29984  wwlksnextproplem3  30002  clwwlkel  30139  1wlkdlem2  30231  trlsegvdeg  30320  eupth2lem3lem1  30321  eupth2lem3lem2  30322  extwwlkfab  30445  numclwlk2lem2f  30470  spansnid  31657  elspansn4  31667  fnpreimac  32766  ccatf1  33048  ccatws1f1olast  33051  swrdrn2  33053  swrdrn3  33054  swrdf1  33055  splfv3  33057  pwrssmgc  33099  suppgsumssiun  33172  wrdpmtrlast  33193  psgnfzto1stlem  33200  cycpmfv1  33213  cycpmfv2  33214  cycpmco2lem2  33227  cycpmco2lem4  33229  cycpmco2lem5  33230  cycpmco2lem6  33231  cycpmco2  33233  cyc3co2  33240  cycpmrn  33243  submarchi  33286  subrdom  33385  fracfld  33408  imaslmod  33452  quslmod  33457  quslmhm  33458  nsgqusf1olem2  33513  lmhmqusker  33516  rhmquskerlem  33524  idlinsubrg  33530  drngidl  33532  rhmpreimaprmidl  33550  qsidomlem2  33552  mxidlprm  33569  opprmxidlabs  33586  qsdrngilem  33593  qsdrngi  33594  qsdrnglem2  33595  idlsrg0g  33605  pidufd  33642  dfufd2lem  33648  fply1  33657  evl1fpws  33663  ressply1evls1  33664  ressply1sub  33669  ply1asclunit  33673  r1plmhm  33709  extvfvcl  33719  evlextv  33725  mplvrpmga  33728  psrmon  33732  psrmonprod  33735  mplmonprod  33737  issply  33744  esplympl  33750  esplyind  33758  drgextlsp  33777  matdim  33799  ply1degltdimlem  33806  lindsunlem  33808  qusdimsum  33812  fedgmullem1  33813  fedgmullem2  33814  fedgmul  33815  extdg1id  33850  evls1fldgencl  33854  irngss  33871  irngnzply1  33875  extdgfialglem1  33876  extdgfialglem2  33877  minplymindeg  33892  minplyirredlem  33894  irredminply  33900  algextdeglem2  33902  constrconj  33929  constrfiss  33935  1smat1  33988  submat1n  33989  lmatfval  33998  lmatcl  34000  mdetpmtr1  34007  madjusmdetlem4  34014  qtopt1  34019  qtophaus  34020  locfinref  34025  zarcls1  34053  zarclsiin  34055  zarmxt1  34064  zarcmplem  34065  rhmpreimacn  34069  ordtrest2NEWlem  34106  elzrhunit  34161  qqhcn  34175  qqhucn  34176  esumel  34231  esumsplit  34237  sigagenss2  34334  elsx  34378  sxbrsigalem0  34455  dya2icoseg  34461  eulerpartlemb  34552  eulerpartlemgvv  34560  iwrdsplit  34571  sseqfv2  34578  probfinmeasb  34612  dstrvprob  34656  dstfrvel  34658  ballotlemrv  34704  signstfvn  34753  signstfvp  34755  signstfveq0  34761  signsvtp  34767  signsvtn  34768  reprsuc  34799  reprpmtf1o  34810  lpadleft  34867  bnj1006  35142  bnj1018g  35145  bnj1018  35146  bnj1121  35167  bnj1398  35216  bnj1450  35232  bnj1501  35249  revpfxsfxrev  35338  swrdrevpfx  35339  pfxwlk  35346  revwlk  35347  swrdwlk  35349  subfacp1lem5  35406  ptpconn  35455  indispconn  35456  cvxsconn  35465  cvmseu  35498  cvmliftmolem2  35504  cvmliftlem7  35513  cvmliftlem10  35516  cvmliftlem13  35518  cvmlift2lem12  35536  satfv1lem  35584  satffunlem1lem2  35625  satffunlem2lem2  35628  satefvfmla1  35647  mrsubcv  35732  mrsubff  35734  mrsubrn  35735  mrsubccat  35740  elmrsubrn  35742  mrsubco  35743  mrsubvrs  35744  mvhf  35780  msubvrs  35782  mclsax  35791  r1peuqusdeg1  35865  linerflx1  36371  linerflx2  36373  fwddifnval  36385  elhf2  36397  neibastop2lem  36582  weiunpo  36687  weiunso  36688  icoreunrn  37641  relowlssretop  37645  sucneqond  37647  matunitlindflem2  37897  poimirlem4  37904  poimirlem20  37920  poimirlem30  37930  broucube  37934  opnmbllem0  37936  areacirclem2  37989  areacirclem4  37991  blssp  38036  sstotbnd2  38054  totbndbnd  38069  prdstotbnd  38074  cnpwstotbnd  38077  heiborlem9  38099  exidcl  38156  exidresid  38159  grpokerinj  38173  iscringd  38278  erimeq2  39043  prter3  39287  toycom  39378  islfld  39467  lshpsmreu  39514  ldualelvbase  39532  ldualssvscl  39563  lkreqN  39575  lkrlspeqN  39576  erng1lem  41392  erngdvlem4  41396  erng0g  41399  erng1r  41400  erngdvlem4-rN  41404  dva0g  41432  dia1dim2  41467  dia1dimid  41468  dia2dimlem5  41473  dvhelvbasei  41493  dvhvaddass  41502  tendoinvcl  41509  tendolinv  41510  tendorinv  41511  dvhgrp  41512  dvhlveclem  41513  cdlemn4  41603  lcfrlem12N  41959  lcfrlem15  41962  lcdvscl  42010  lcdlssvscl  42011  lcdvsass  42012  lcdvs0N  42021  mapdincl  42066  mapdin  42067  mapdlsmcl  42068  mapdcnvatN  42071  mapdpglem2  42078  mapdpglem12  42088  mapdpglem18  42094  mapdpglem21  42097  mapdpglem22  42098  mapdpglem28  42106  mapdpglem30  42107  hdmaprnlem3N  42255  hdmaprnlem3uN  42256  hdmaprnlem7N  42260  hdmaprnlem8N  42261  hdmaprnlem9N  42262  hdmaprnlem3eN  42263  hdmaprnlem16N  42267  hgmapdcl  42295  hgmapval1  42298  hgmaprnlem4N  42304  hdmapinvlem1  42323  fzadd2d  42377  aks6d1c2lem4  42526  sticksstones1  42545  sticksstones8  42552  sticksstones9  42553  sticksstones10  42554  sticksstones11  42555  sticksstones17  42562  sticksstones18  42563  aks6d1c6lem4  42572  rhmqusspan  42584  aks5lem2  42586  mhmcopsr  42946  evlsbagval  42956  evlsevl  42961  evlvvval  42962  evlvvvallem  42963  selvcllem2  42965  evlselv  42974  mhpind  42981  fltnltalem  43049  wepwsolem  43428  kercvrlsm  43469  dfacbasgrp  43494  onexomgt  43627  onexoegt  43630  onov0suclim  43660  cantnftermord  43706  cantnf2  43711  omcl2  43719  ofoaf  43741  ofoafo  43742  grurankcld  44618  grumnudlem  44670  grumnud  44671  inaex  44682  gruex  44683  dvconstbi  44719  cncmpmax  45421  iooabslt  45888  fmul01lt1lem2  45974  limciccioolb  46010  limcicciooub  46024  limsuppnfdlem  46088  climrescn  46135  climxrrelem  46136  climxrre  46137  liminflimsupxrre  46204  xlimmnfvlem2  46220  xlimpnfvlem2  46224  fsumcncf  46265  ioccncflimc  46272  icocncflimc  46276  cncfiooicclem1  46280  dvbdfbdioolem2  46316  dvnmul  46330  dvnprodlem1  46333  stoweidlem26  46413  stoweidlem34  46421  stoweidlem48  46435  stoweidlem59  46446  dirkercncflem3  46492  fourierdlem32  46526  fourierdlem41  46535  fourierdlem51  46544  fourierdlem63  46556  fourierdlem82  46575  fourierdlem85  46578  fourierdlem93  46586  fourierdlem111  46604  fourierdlem114  46607  etransclem35  46656  hoicvr  46935  hspdifhsp  47003  opnvonmbllem1  47019  ovnovollem1  47043  mbfresmf  47126  smfaddlem1  47150  smfsuplem1  47198  smflimsuplem5  47211  chnerlem2  47270  setsidel  47765  setsnidel  47766  imasetpreimafvbijlemf  47790  prelspr  47875  upgrimpths  48298  gpgprismgr4cycllem9  48492  rngccatidALTV  48661  rhmsubcALTVlem3  48672  funcringcsetcALTV2lem3  48681  funcringcsetcALTV2lem8  48686  ringccatidALTV  48695  funcringcsetclem3ALTV  48704  funcringcsetclem8ALTV  48709  srhmsubcALTVlem1  48712  srhmsubcALTV  48714  lcosslsp  48827  nnolog2flm1  48979  ffvbr  49244  glbprlem  49353  topdlat  49392  catprs  49399  iinfsubc  49446  iinfconstbaslem  49453  imaid  49542  fthcomf  49545  uptr2  49609  natoppf2  49618  natoppfb  49619  swapf2  49662  swapfiso  49673  swapciso  49674  oppc1stflem  49675  cofuswapf2  49683  fuco22natlem  49733  fucoppcffth  49799  oppcthinco  49827  oppcthinendcALT  49829  thinccisod  49842  termco  49869  termchommo  49873  termcid  49874  termcterm  49901  termcterm2  49902  diagciso  49927  diagcic  49928  funcsn  49929  uobeqterm  49934  mndtccatid  49975  grptcmon  49981  grptcepi  49982  2arwcat  49988  lanval2  50015  ranval2  50018  lanup  50029  ranup  50030  lmddu  50055