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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728  df-clel 2814

This theorem is referenced by:  3eltr4d  2852  rspc2vd  3888  disjxiun  5078  eldmressnsn  5946  elimdelov  7403  elovmpt3rab1  7561  fnwelem  8003  tfrlem13  8252  tz7.44-2  8269  omordi  8428  oneo  8443  omeulem2  8445  oeordi  8449  oeeui  8464  nnneo  8516  erref  8549  en1uniel  8853  en1unielOLD  8854  omxpenlem  8898  unblem3  9112  dffi3  9234  ordtypelem10  9330  oismo  9343  cantnff  9476  cantnfp1lem3  9482  cantnflem1  9491  cnfcom  9502  r1ordg  9580  r1pwss  9586  rankwflemb  9595  r1elwf  9598  rankidb  9602  rankonidlem  9630  fseqenlem2  9827  dfac12lem1  9945  dfac12lem2  9946  pwsdompw  10006  ackbij2lem3  10043  ackbij2  10045  cfsmolem  10072  hsmexlem4  10231  ttukeylem3  10313  ttukeylem7  10317  iundom2g  10342  fpwwe2lem8  10440  canthwelem  10452  pwfseqlem4  10464  winalim2  10498  r1wunlim  10539  tskmid  10642  fzopth  13339  predfz  13427  fzoss2  13461  fz1fzo0m1  13481  fzo0addel  13487  fzo0addelr  13488  fzosubel3  13494  elfzomin  13505  elfzonlteqm1  13509  fzoend  13524  fzofzp1  13530  fzofzp1b  13531  peano2fzor  13540  zmodfzo  13660  seqf1olem2  13809  bcn2  14079  swrdccat2  14427  pfxccat1  14460  swrdswrd  14463  pfxccatin12  14491  splfv1  14513  revcl  14519  revlen  14520  revccat  14524  revrev  14525  repswpfx  14543  cshwidxmod  14561  revco  14592  limsupgre  15235  summolem2a  15472  fsumm1  15508  fsumcom2  15531  prodmolem2a  15689  fprodm1  15722  fprodcom2  15739  prmreclem4  16665  prmreclem5  16666  vdwapid1  16721  vdwlem5  16731  vdwlem8  16734  vdwnnlem2  16742  ramub1lem1  16772  ramub1lem2  16773  mrieqvlemd  17383  mreexd  17396  mreexexlemd  17398  catcocl  17439  catass  17440  moni  17493  epii  17500  inviso1  17523  episect  17542  invisoinvl  17547  catsubcat  17599  subccocl  17605  fullsubc  17610  funcco  17631  resf2nd  17655  funcres  17656  fthepi  17689  nati  17716  arwhoma  17805  catccatid  17866  resscatc  17869  catcisolem  17870  catcoppccl  17877  catcoppcclOLD  17878  catcfuccl  17879  catcfucclOLD  17880  estrreslem2  17900  funcestrcsetclem3  17904  funcestrcsetclem8  17909  equivestrcsetc  17914  funcsetcestrclem3  17918  funcsetcestrclem8  17924  xpcco  17945  xpcco2  17949  xpccatid  17950  prfcl  17965  catcxpccl  17969  catcxpcclOLD  17970  curf12  17990  curf1cl  17991  curf2  17992  curf2cl  17994  curfcl  17995  uncf2  18000  uncfcurf  18002  diag12  18007  diag2  18008  curf2ndf  18010  hofcl  18022  oppchofcl  18023  oyoncl  18033  yonedalem3a  18037  yonedalem4b  18039  yonedalem22  18041  yonedalem3b  18042  yonedalem3  18043  yonedainv  18044  yonffthlem  18045  latcl2  18199  latlem  18200  latjcom  18210  latmcom  18226  clatlem  18265  clatlubcl2  18267  clatglbcl2  18269  acsfiindd  18316  gsumpropd2lem  18408  mndpropd  18455  imasmnd  18468  frmdmnd  18543  frmdgsum  18546  grpsubpropd2  18726  imasgrp  18736  subg0  18806  0ghm  18893  resghm2  18896  ghmco  18899  pwsdiagghm  18907  psgnunilem1  19146  psgnunilem5  19147  psgnunilem2  19148  psgnunilem3  19149  sylow1lem4  19251  sylow1lem5  19252  efglem  19367  efgtf  19373  efginvrel2  19378  efginvrel1  19379  efgsdmi  19383  efgs1b  19387  efgsres  19389  efgsfo  19390  efgredleme  19394  efgredlemc  19396  efgredlem  19398  efgcpbllemb  19406  frgp0  19411  frgpadd  19414  frgpinv  19415  vrgpf  19419  vrgpinv  19420  frgpuplem  19423  frgpup1  19426  frgpup2  19427  frgpup3lem  19428  frgpnabllem1  19519  frgpnabllem2  19520  gsumval3  19553  dprdfid  19665  dprdsn  19684  dprd2da  19690  dpjidcl  19706  pgpfac1lem2  19723  pgpfaclem3  19731  ablsimpg1gend  19753  ablsimpgprmd  19763  ringpropd  19866  imasring  19903  qusring2  19904  pwsco1rhm  20027  pwsco2rhm  20028  subrgunit  20087  pwsdiagrhm  20103  cntzsdrg  20115  isabvd  20125  lmodprop2d  20230  islssd  20242  prdsvscacl  20275  prdslmodd  20276  islmhm2  20345  lmhmco  20350  lmhmplusg  20351  lmhmvsca  20352  lmhmpropd  20380  lsppreli  20397  lspsnel4  20431  lssacsex  20451  lspsnat  20452  qus1  20551  qusrhm  20553  znf1o  20804  cssmre  20943  dsmmlss  20996  frlmsplit2  21025  frlmbas3  21028  frlmup1  21050  assapropd  21121  psr0cl  21208  psrnegcl  21210  psr1cl  21216  resspsrmul  21231  subrgpsr  21233  mvrf  21238  mplmon  21281  mplcoe1  21283  subrgasclcl  21320  mplind  21323  evlslem1  21337  subrgply1  21449  psrplusgpropd  21452  ply1coe  21512  cply1coe0bi  21516  lply1binomsc  21523  evls1val  21531  evls1rhm  21533  evl1val  21540  evl1rhm  21543  pf1ind  21566  evl1scvarpw  21574  matbas2i  21616  matplusg2  21621  matvsca2  21622  matsubgcell  21628  matvscacell  21630  mpomatmul  21640  mavmulval  21739  mavmulcl  21741  mavmulass  21743  mavmul0  21746  mavmumamul1  21749  m1detdiag  21791  cramerimplem2  21878  mat2pmatmul  21925  mat2pmatlin  21929  monmatcollpw  21973  pmatcollpwfi  21976  mply1topmatcl  21999  pm2mpghm  22010  pm2mpmhmlem2  22013  pm2mp  22019  chpmat1dlem  22029  chpmat1d  22030  chpdmatlem0  22031  chpscmat  22036  chpscmatgsumbin  22038  chpscmatgsummon  22039  chfacfscmulcl  22051  cpmadugsumlemB  22068  cpmadugsumlemC  22069  chcoeffeqlem  22079  cldmreon  22290  neiptopreu  22329  maxlp  22343  ordttopon  22389  ordtrest2lem  22399  cnprcl2  22447  lmcnp  22500  resthauslem  22559  hauscmplem  22602  1stcfb  22641  2ndcctbss  22651  2ndcomap  22654  dis2ndc  22656  loclly  22683  hausllycmp  22690  locfincmp  22722  dissnref  22724  kgeni  22733  kgenidm  22743  ptpjpre2  22776  xkoopn  22785  txopn  22798  ptpjopn  22808  ptcldmpt  22810  ptcls  22812  pthaus  22834  txkgen  22848  xkohaus  22849  xkopt  22851  txconn  22885  imastps  22917  kqid  22924  kqopn  22930  kqcld  22931  isr0  22933  indishmph  22994  pt1hmeo  23002  ptuncnv  23003  ptunhmeo  23004  t0kq  23014  filconn  23079  uzrest  23093  uffixsn  23121  fmfnfmlem2  23151  flimss2  23168  flimss1  23169  flimclslem  23180  flfcnp  23200  fclsfnflim  23223  uffclsflim  23227  fcfelbas  23232  alexsublem  23240  alexsub  23241  cnextcn  23263  cnextfres1  23264  cnextfres  23265  tmdgsum  23291  distgp  23295  indistgp  23296  symgtgp  23302  ghmcnp  23311  qustgpopn  23316  qustgplem  23317  qustgphaus  23319  prdstmdd  23320  prdstgpd  23321  tsmsid  23336  tsmssubm  23339  tsmsmhm  23342  tsmsadd  23343  tsmssplit  23348  utop2nei  23447  utop3cls  23448  neipcfilu  23493  cnextucn  23500  ucnextcn  23501  blpnfctr  23634  lpbl  23704  met2ndci  23723  tmsxps  23737  metcnpi  23745  metcnpi2  23746  metcnpi3  23747  metustid  23755  metustsym  23756  metustexhalf  23757  subgngp  23836  ngptgp  23837  sranlm  23893  nlmvscn  23896  nrginvrcn  23901  lssnlm  23910  nghmcn  23954  iccntr  24029  icccmplem2  24031  msdcn  24049  cncfmptc  24120  cncfmptid  24121  cncfmpt2f  24123  icoopnst  24147  iocopnst  24148  nmoleub2lem3  24323  nmoleub3  24327  nmhmcn  24328  ipcn  24455  cfilfcls  24483  caucfil  24492  equivcau  24509  caubl  24517  flimcfil  24523  cmssmscld  24559  rrxdstprj1  24618  minveclem3b  24637  minveclem4  24641  ovolicc2lem3  24728  ovolicc2lem4  24729  opnmbllem  24810  vitalilem2  24818  mbfsup  24873  mbfinf  24874  mbfi1fseqlem4  24928  limccnp  25100  limccnp2  25101  dvreslem  25118  dvres2lem  25119  dvidlem  25124  dvcnp2  25129  dvcn  25130  dvaddbr  25147  dvmulbr  25148  dvcmul  25153  dvcof  25157  dvcnvlem  25185  dvef  25189  rollelem  25198  dvlip2  25204  dvivthlem1  25217  dvivth  25219  lhop2  25224  lhop  25225  dvcnvrelem1  25226  dvcnvrelem2  25227  dvcnvre  25228  ply1rem  25373  fta1blem  25378  plycpn  25494  plyrem  25510  tayl0  25566  dvtaylp  25574  dvntaylp  25575  dvntaylp0  25576  taylthlem1  25577  taylthlem2  25578  ulmdvlem3  25606  psercn  25630  pserdv  25633  abelth  25645  efabl  25751  efopnlem1  25856  loglesqrt  25956  relogbf  25986  efrlim  26164  dchrghm  26449  dchrptlem3  26459  tgbtwntriv2  26893  tgbtwnne  26896  ercgrg  26923  tgidinside  26977  tgbtwnconn1  26981  tglnne  27034  tglnne0  27046  tglnpt2  27047  tglineneq  27050  ncolncol  27052  coltr3  27054  mirln  27082  mirln2  27083  mirconn  27084  krippenlem  27096  footexALT  27124  footexlem1  27125  footexlem2  27126  colperpexlem3  27138  mideulem2  27140  opphllem  27141  oppne3  27149  opphllem1  27153  opphllem2  27154  opphllem4  27156  oppperpex  27159  opphl  27160  hlpasch  27162  hpgerlem  27171  colhp  27176  midbtwn  27185  lmieu  27190  lmiisolem  27202  sacgr  27237  f1otrg  27277  f1otrge  27278  ebtwntg  27395  ecgrtg  27396  eengtrkg  27399  eengtrkge  27400  upgr1eop  27530  usgredg3  27628  uspgr1eop  27659  usgr1eop  27662  vtxdun  27893  vtxdfiun  27894  1loopgruspgr  27912  1loopgrvd2  27915  1hevtxdg1  27918  1egrvtxdg1  27921  1egrvtxdg0  27923  umgr2v2e  27937  wlkres  28083  wlkp1lem4  28089  wlkp1  28094  wwlksm1edg  28291  wwlksnext  28303  wwlksnextproplem3  28321  clwwlkel  28455  1wlkdlem2  28547  trlsegvdeg  28636  eupth2lem3lem1  28637  eupth2lem3lem2  28638  extwwlkfab  28761  numclwlk2lem2f  28786  spansnid  29970  elspansn4  29980  fnpreimac  31053  ccatf1  31268  swrdrn2  31271  swrdrn3  31272  swrdf1  31273  splfv3  31275  pwrssmgc  31323  psgnfzto1stlem  31412  cycpmfv1  31425  cycpmfv2  31426  cycpmco2lem2  31439  cycpmco2lem4  31441  cycpmco2lem5  31442  cycpmco2lem6  31443  cycpmco2  31445  cyc3co2  31452  cycpmrn  31455  submarchi  31485  imaslmod  31598  quslmod  31599  quslmhm  31600  nsgqusf1olem2  31644  rhmpreimaidl  31648  idlinsubrg  31653  lidlnsg  31666  rhmpreimaprmidl  31672  qsidomlem2  31674  mxidlprm  31685  idlsrg0g  31696  fply1  31712  ply1fermltl  31715  drgextlsp  31726  matdim  31743  lindsunlem  31750  qusdimsum  31754  fedgmullem1  31755  fedgmullem2  31756  fedgmul  31757  extdg1id  31783  1smat1  31799  submat1n  31800  lmatfval  31809  lmatcl  31811  mdetpmtr1  31818  madjusmdetlem4  31825  qtopt1  31830  qtophaus  31831  locfinref  31836  zarcls1  31864  zarclsiin  31866  zarmxt1  31875  zarcmplem  31876  rhmpreimacn  31880  ordtrest2NEWlem  31917  elzrhunit  31974  qqhcn  31986  qqhucn  31987  esumel  32060  esumsplit  32066  sigagenss2  32163  elsx  32207  sxbrsigalem0  32283  dya2icoseg  32289  eulerpartlemb  32380  eulerpartlemgvv  32388  iwrdsplit  32399  sseqfv2  32406  probfinmeasb  32440  dstrvprob  32483  dstfrvel  32485  ballotlemrv  32531  signstfvn  32593  signstfvp  32595  signstfveq0  32601  signsvtp  32607  signsvtn  32608  reprsuc  32640  reprpmtf1o  32651  lpadleft  32708  bnj1006  32985  bnj1018g  32988  bnj1018  32989  bnj1121  33010  bnj1398  33059  bnj1450  33075  bnj1501  33092  revpfxsfxrev  33122  swrdrevpfx  33123  pfxwlk  33130  revwlk  33131  swrdwlk  33133  subfacp1lem5  33191  ptpconn  33240  indispconn  33241  cvxsconn  33250  cvmseu  33283  cvmliftmolem2  33289  cvmliftlem7  33298  cvmliftlem10  33301  cvmliftlem13  33303  cvmlift2lem12  33321  satfv1lem  33369  satffunlem1lem2  33410  satffunlem2lem2  33413  satefvfmla1  33432  mrsubcv  33517  mrsubff  33519  mrsubrn  33520  mrsubccat  33525  elmrsubrn  33527  mrsubco  33528  mrsubvrs  33529  mvhf  33565  msubvrs  33567  mclsax  33576  naddelim  33883  nodenselem5  33936  nosupres  33955  noinfres  33970  sltlpss  34132  linerflx1  34496  linerflx2  34498  fwddifnval  34510  elhf2  34522  neibastop2lem  34594  icoreunrn  35574  relowlssretop  35578  sucneqond  35580  matunitlindflem2  35818  poimirlem4  35825  poimirlem20  35841  poimirlem30  35851  broucube  35855  opnmbllem0  35857  areacirclem2  35910  areacirclem4  35912  blssp  35958  sstotbnd2  35976  totbndbnd  35991  prdstotbnd  35996  cnpwstotbnd  35999  heiborlem9  36021  exidcl  36078  exidresid  36081  grpokerinj  36095  iscringd  36200  erim2  36831  prter3  36938  toycom  37029  islfld  37118  lshpsmreu  37165  ldualelvbase  37183  ldualssvscl  37214  lkreqN  37226  lkrlspeqN  37227  erng1lem  39043  erngdvlem4  39047  erng0g  39050  erng1r  39051  erngdvlem4-rN  39055  dva0g  39083  dia1dim2  39118  dia1dimid  39119  dia2dimlem5  39124  dvhelvbasei  39144  dvhvaddass  39153  tendoinvcl  39160  tendolinv  39161  tendorinv  39162  dvhgrp  39163  dvhlveclem  39164  cdlemn4  39254  lcfrlem12N  39610  lcfrlem15  39613  lcdvscl  39661  lcdlssvscl  39662  lcdvsass  39663  lcdvs0N  39672  mapdincl  39717  mapdin  39718  mapdlsmcl  39719  mapdcnvatN  39722  mapdpglem2  39729  mapdpglem12  39739  mapdpglem18  39745  mapdpglem21  39748  mapdpglem22  39749  mapdpglem28  39757  mapdpglem30  39758  hdmaprnlem3N  39906  hdmaprnlem3uN  39907  hdmaprnlem7N  39911  hdmaprnlem8N  39912  hdmaprnlem9N  39913  hdmaprnlem3eN  39914  hdmaprnlem16N  39918  hgmapdcl  39946  hgmapval1  39949  hgmaprnlem4N  39955  hdmapinvlem1  39974  fzadd2d  40028  sticksstones1  40144  sticksstones8  40151  sticksstones9  40152  sticksstones10  40153  sticksstones11  40154  sticksstones17  40161  sticksstones18  40162  fnsnbt  40245  selvval2lem2  40262  selvval2lem4  40265  evlsbagval  40312  mhpind  40320  mhphf  40322  fltnltalem  40536  wepwsolem  40905  kercvrlsm  40946  dfacbasgrp  40971  imo72b2lem0  41814  grurankcld  41889  grumnudlem  41941  grumnud  41942  inaex  41953  gruex  41954  dvconstbi  41990  cncmpmax  42613  iooabslt  43086  fmul01lt1lem2  43175  limciccioolb  43211  limcicciooub  43227  limsuppnfdlem  43291  climrescn  43338  climxrrelem  43339  climxrre  43340  liminflimsupxrre  43407  xlimmnfvlem2  43423  xlimpnfvlem2  43427  fsumcncf  43468  ioccncflimc  43475  icocncflimc  43479  cncfiooicclem1  43483  dvbdfbdioolem2  43519  dvnmul  43533  stoweidlem26  43616  stoweidlem34  43624  stoweidlem48  43638  stoweidlem59  43649  dirkercncflem3  43695  fourierdlem32  43729  fourierdlem41  43738  fourierdlem51  43747  fourierdlem63  43759  fourierdlem82  43778  fourierdlem85  43781  fourierdlem93  43789  fourierdlem111  43807  fourierdlem114  43810  etransclem35  43859  hspdifhsp  44204  opnvonmbllem1  44220  ovnovollem1  44244  mbfresmf  44327  smfaddlem1  44351  smfsuplem1  44398  smflimsuplem5  44411  fzoopth  44877  setsidel  44886  setsnidel  44887  imasetpreimafvbijlemf  44911  prelspr  44996  rnghmsubcsetclem1  45591  rngccatidALTV  45605  zrinitorngc  45616  zrtermorngc  45617  zrzeroorngc  45618  rhmsubcsetclem1  45637  rhmsubcrngclem1  45643  funcringcsetcALTV2lem3  45654  funcringcsetcALTV2lem8  45659  ringccatidALTV  45668  funcringcsetclem3ALTV  45677  funcringcsetclem8ALTV  45682  irinitoringc  45685  zrtermoringc  45686  zrninitoringc  45687  nzerooringczr  45688  srhmsubclem2  45690  srhmsubc  45692  srhmsubcALTVlem1  45708  srhmsubcALTV  45710  rhmsubcALTVlem3  45722  lcosslsp  45837  nnolog2flm1  45994  glbprlem  46317  topdlat  46348  catprs  46350  mndtccatid  46432  grptcmon  46435  grptcepi  46436