Theorem eleqtrrd 2837

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809

This theorem is referenced by:  3eltr4d  2849  rspc2vd  3922  disjxiun  5116  eldmressnsn  6011  fnsnbg  7155  elimdelov  7501  elovmpt3rab1  7665  fnwelem  8128  tfrlem13  8402  tz7.44-2  8419  omordi  8576  oneo  8591  omeulem2  8593  oeordi  8597  oeeui  8612  nnneo  8665  naddelim  8696  erref  8737  en1uniel  9041  omxpenlem  9085  unblem3  9300  dffi3  9441  ordtypelem10  9539  oismo  9552  cantnff  9686  cantnfp1lem3  9692  cantnflem1  9701  cnfcom  9712  r1ordg  9790  r1pwss  9796  rankwflemb  9805  r1elwf  9808  rankidb  9812  rankonidlem  9840  fseqenlem2  10037  dfac12lem1  10156  dfac12lem2  10157  pwsdompw  10215  ackbij2lem3  10252  ackbij2  10254  cfsmolem  10282  hsmexlem4  10441  ttukeylem3  10523  ttukeylem7  10527  iundom2g  10552  fpwwe2lem8  10650  canthwelem  10662  pwfseqlem4  10674  winalim2  10708  r1wunlim  10749  tskmid  10852  fzopth  13576  predfz  13668  fzoss2  13702  fz1fzo0m1  13725  fzo0addel  13732  fzo0addelr  13733  elfzoext  13736  fzosubel3  13740  elfzomin  13751  elfzonlteqm1  13755  fzoend  13771  fzoopth  13776  fzofzp1  13778  fzofzp1b  13779  peano2fzor  13788  zmodfzo  13909  seqf1olem2  14058  bcn2  14335  swrdccat2  14685  pfxccat1  14718  swrdswrd  14721  pfxccatin12  14749  splfv1  14771  revcl  14777  revlen  14778  revccat  14782  revrev  14783  repswpfx  14801  cshwidxmod  14819  revco  14851  limsupgre  15495  summolem2a  15729  fsumm1  15765  fsumcom2  15788  prodmolem2a  15948  fprodm1  15981  fprodcom2  15998  prmreclem4  16937  prmreclem5  16938  vdwapid1  16993  vdwlem5  17003  vdwlem8  17006  vdwnnlem2  17014  ramub1lem1  17044  ramub1lem2  17045  mrieqvlemd  17639  mreexd  17652  mreexexlemd  17654  catcocl  17695  catass  17696  moni  17747  epii  17754  inviso1  17777  episect  17796  invisoinvl  17801  catsubcat  17850  subccocl  17856  fullsubc  17861  funcco  17882  resf2nd  17906  funcres  17907  fthepi  17941  nati  17969  arwhoma  18056  catccatid  18117  resscatc  18120  catcisolem  18121  catcoppccl  18128  catcfuccl  18129  estrreslem2  18148  funcestrcsetclem3  18152  funcestrcsetclem8  18157  equivestrcsetc  18162  funcsetcestrclem3  18166  funcsetcestrclem8  18172  xpcco  18193  xpcco2  18197  xpccatid  18198  prfcl  18213  catcxpccl  18217  curf12  18237  curf1cl  18238  curf2  18239  curf2cl  18241  curfcl  18242  uncf2  18247  uncfcurf  18249  diag12  18254  diag2  18255  curf2ndf  18257  hofcl  18269  oppchofcl  18270  oyoncl  18280  yonedalem3a  18284  yonedalem4b  18286  yonedalem22  18288  yonedalem3b  18289  yonedalem3  18290  yonedainv  18291  yonffthlem  18292  latcl2  18444  latlem  18445  latjcom  18455  latmcom  18471  clatlem  18510  clatlubcl2  18512  clatglbcl2  18514  acsfiindd  18561  gsumpropd2lem  18655  sgrppropd  18707  mndpropd  18735  imasmnd  18751  frmdmnd  18835  frmdgsum  18838  grpsubpropd2  19027  imasgrp  19037  subg0  19113  0ghm  19211  resghm2  19214  ghmco  19217  pwsdiagghm  19225  ghmqusnsglem2  19262  ghmqusnsg  19263  ghmquskerlem2  19266  ghmquskerlem3  19267  ghmqusker  19268  psgnunilem1  19472  psgnunilem5  19473  psgnunilem2  19474  psgnunilem3  19475  sylow1lem4  19580  sylow1lem5  19581  efglem  19695  efgtf  19701  efginvrel2  19706  efginvrel1  19707  efgsdmi  19711  efgs1b  19715  efgsres  19717  efgsfo  19718  efgredleme  19722  efgredlemc  19724  efgredlem  19726  efgcpbllemb  19734  frgp0  19739  frgpadd  19742  frgpinv  19743  vrgpf  19747  vrgpinv  19748  frgpuplem  19751  frgpup1  19754  frgpup2  19755  frgpup3lem  19756  frgpnabllem1  19852  frgpnabllem2  19853  gsumval3  19886  dprdfid  19998  dprdsn  20017  dprd2da  20023  dpjidcl  20039  pgpfac1lem2  20056  pgpfaclem3  20064  ablsimpg1gend  20086  ablsimpgprmd  20096  rngpropd  20132  imasrng  20135  ringpropd  20246  imasring  20288  qusring2  20292  pwsco1rhm  20460  pwsco2rhm  20461  lringuplu  20502  subrgunit  20548  pwsdiagrhm  20565  rnghmsubcsetclem1  20589  zrinitorngc  20600  zrtermorngc  20601  zrzeroorngc  20602  rhmsubcsetclem1  20618  rhmsubcrngclem1  20624  zrtermoringc  20633  zrninitoringc  20634  srhmsubclem2  20636  srhmsubc  20638  cntzsdrg  20760  isabvd  20770  lmodprop2d  20879  islssd  20890  prdsvscacl  20923  prdslmodd  20924  islmhm2  20994  lmhmco  20999  lmhmplusg  21000  lmhmvsca  21001  lmhmpropd  21029  lsppreli  21046  ellspsn4  21083  lssacsex  21103  lspsnat  21104  lidlnsg  21207  qus2idrng  21232  qus1  21233  qusrhm  21235  rhmpreimaidl  21236  rhmqusnsg  21244  rngqiprngghmlem1  21246  rngqiprngfulem1  21270  irinitoringc  21438  nzerooringczr  21439  znf1o  21510  cssmre  21651  dsmmlss  21702  frlmsplit2  21731  frlmbas3  21734  frlmup1  21756  assapropd  21830  psr0cl  21910  psrnegcl  21912  psr1cl  21919  resspsrmul  21934  subrgpsr  21936  mvrf  21943  mplmon  21991  mplcoe1  21993  subrgasclcl  22023  mplind  22026  evlslem1  22038  subrgply1  22166  psrplusgpropd  22169  ply1coe  22234  cply1coe0bi  22238  lply1binomsc  22247  ply1fermltlchr  22248  evls1val  22256  evls1rhm  22258  evl1val  22265  evl1rhm  22268  pf1ind  22291  evl1scvarpw  22299  evls1fpws  22305  mhmcompl  22316  rhmply1  22322  matbas2i  22358  matplusg2  22363  matvsca2  22364  matsubgcell  22370  matvscacell  22372  mpomatmul  22382  mavmulval  22481  mavmulcl  22483  mavmulass  22485  mavmul0  22488  mavmumamul1  22491  m1detdiag  22533  cramerimplem2  22620  mat2pmatmul  22667  mat2pmatlin  22671  monmatcollpw  22715  pmatcollpwfi  22718  mply1topmatcl  22741  pm2mpghm  22752  pm2mpmhmlem2  22755  pm2mp  22761  chpmat1dlem  22771  chpmat1d  22772  chpdmatlem0  22773  chpscmat  22778  chpscmatgsumbin  22780  chpscmatgsummon  22781  chfacfscmulcl  22793  cpmadugsumlemB  22810  cpmadugsumlemC  22811  chcoeffeqlem  22821  cldmreon  23030  neiptopreu  23069  maxlp  23083  ordttopon  23129  ordtrest2lem  23139  cnprcl2  23187  lmcnp  23240  resthauslem  23299  hauscmplem  23342  1stcfb  23381  2ndcctbss  23391  2ndcomap  23394  dis2ndc  23396  loclly  23423  hausllycmp  23430  locfincmp  23462  dissnref  23464  kgeni  23473  kgenidm  23483  ptpjpre2  23516  xkoopn  23525  txopn  23538  ptpjopn  23548  ptcldmpt  23550  ptcls  23552  pthaus  23574  txkgen  23588  xkohaus  23589  xkopt  23591  txconn  23625  imastps  23657  kqid  23664  kqopn  23670  kqcld  23671  isr0  23673  indishmph  23734  pt1hmeo  23742  ptuncnv  23743  ptunhmeo  23744  t0kq  23754  filconn  23819  uzrest  23833  uffixsn  23861  fmfnfmlem2  23891  flimss2  23908  flimss1  23909  flimclslem  23920  flfcnp  23940  fclsfnflim  23963  uffclsflim  23967  fcfelbas  23972  alexsublem  23980  alexsub  23981  cnextcn  24003  cnextfres1  24004  cnextfres  24005  tmdgsum  24031  distgp  24035  indistgp  24036  symgtgp  24042  ghmcnp  24051  qustgpopn  24056  qustgplem  24057  qustgphaus  24059  prdstmdd  24060  prdstgpd  24061  tsmsid  24076  tsmssubm  24079  tsmsmhm  24082  tsmsadd  24083  tsmssplit  24088  utop2nei  24187  utop3cls  24188  neipcfilu  24232  cnextucn  24239  ucnextcn  24240  blpnfctr  24373  lpbl  24440  met2ndci  24459  tmsxps  24473  metcnpi  24481  metcnpi2  24482  metcnpi3  24483  metustid  24491  metustsym  24492  metustexhalf  24493  subgngp  24572  ngptgp  24573  sranlm  24621  nlmvscn  24624  nrginvrcn  24629  lssnlm  24638  nghmcn  24682  iccntr  24759  icccmplem2  24761  msdcn  24779  cncfmptc  24854  cncfmptid  24855  cncfmpt2f  24857  icoopnst  24885  iocopnst  24886  nmoleub2lem3  25064  nmoleub3  25068  nmhmcn  25069  ipcn  25196  cfilfcls  25224  caucfil  25233  equivcau  25250  caubl  25258  flimcfil  25264  cmssmscld  25300  rrxdstprj1  25359  minveclem3b  25378  minveclem4  25382  mulcncf  25396  ovolicc2lem3  25470  ovolicc2lem4  25471  opnmbllem  25552  vitalilem2  25560  mbfsup  25615  mbfinf  25616  mbfi1fseqlem4  25669  limccnp  25842  limccnp2  25843  dvreslem  25860  dvres2lem  25861  dvidlem  25866  dvcnp2  25871  dvcnp2OLD  25872  dvcn  25873  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvcmul  25897  dvcof  25902  dvcnvlem  25930  dvef  25934  rollelem  25943  dvlip2  25950  dvivthlem1  25963  dvivth  25965  lhop2  25970  lhop  25971  dvcnvrelem1  25972  dvcnvrelem2  25973  dvcnvre  25974  ply1rem  26121  fta1blem  26126  plycpn  26247  plyrem  26263  tayl0  26319  dvtaylp  26328  dvntaylp  26329  dvntaylp0  26330  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  ulmdvlem3  26361  psercn  26386  pserdv  26389  abelth  26401  efabl  26509  efopnlem1  26615  loglesqrt  26721  relogbf  26751  efrlim  26929  efrlimOLD  26930  dchrghm  27217  dchrptlem3  27227  nodenselem5  27650  nosupres  27669  noinfres  27684  sltlpss  27862  precsexlem11  28158  noseq0  28213  noseqp1  28214  noseqrdgfn  28229  noseqrdgsuc  28231  tgbtwntriv2  28412  tgbtwnne  28415  ercgrg  28442  tgidinside  28496  tgbtwnconn1  28500  tglnne  28553  tglnne0  28565  tglnpt2  28566  tglineneq  28569  ncolncol  28571  coltr3  28573  mirln  28601  mirln2  28602  mirconn  28603  krippenlem  28615  footexALT  28643  footexlem1  28644  footexlem2  28645  colperpexlem3  28657  mideulem2  28659  opphllem  28660  oppne3  28668  opphllem1  28672  opphllem2  28673  opphllem4  28675  oppperpex  28678  opphl  28679  hlpasch  28681  hpgerlem  28690  colhp  28695  midbtwn  28704  lmieu  28709  lmiisolem  28721  sacgr  28756  f1otrg  28796  f1otrge  28797  ebtwntg  28907  ecgrtg  28908  eengtrkg  28911  eengtrkge  28912  upgr1eop  29040  usgredg3  29141  uspgr1eop  29172  usgr1eop  29175  vtxdun  29407  vtxdfiun  29408  1loopgruspgr  29426  1loopgrvd2  29429  1hevtxdg1  29432  1egrvtxdg1  29435  1egrvtxdg0  29437  umgr2v2e  29451  wlkres  29596  wlkp1lem4  29602  wlkp1  29607  cyclnumvtx  29728  wwlksm1edg  29809  wwlksnext  29821  wwlksnextproplem3  29839  clwwlkel  29973  1wlkdlem2  30065  trlsegvdeg  30154  eupth2lem3lem1  30155  eupth2lem3lem2  30156  extwwlkfab  30279  numclwlk2lem2f  30304  spansnid  31490  elspansn4  31500  fnpreimac  32595  ccatf1  32870  ccatws1f1olast  32874  swrdrn2  32876  swrdrn3  32877  swrdf1  32878  splfv3  32880  pwrssmgc  32926  pfxchn  32935  chnind  32937  chnub  32938  chnlt  32939  wrdpmtrlast  33050  psgnfzto1stlem  33057  cycpmfv1  33070  cycpmfv2  33071  cycpmco2lem2  33084  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2  33090  cyc3co2  33097  cycpmrn  33100  submarchi  33130  subrdom  33225  fracfld  33248  imaslmod  33314  quslmod  33319  quslmhm  33320  nsgqusf1olem2  33375  lmhmqusker  33378  rhmquskerlem  33386  idlinsubrg  33392  drngidl  33394  rhmpreimaprmidl  33412  qsidomlem2  33414  mxidlprm  33431  opprmxidlabs  33448  qsdrngilem  33455  qsdrngi  33456  qsdrnglem2  33457  idlsrg0g  33467  pidufd  33504  dfufd2lem  33510  fply1  33517  evl1fpws  33523  ressply1evls1  33524  ressply1sub  33529  ply1asclunit  33533  r1plmhm  33565  drgextlsp  33579  matdim  33601  ply1degltdimlem  33608  lindsunlem  33610  qusdimsum  33614  fedgmullem1  33615  fedgmullem2  33616  fedgmul  33617  extdg1id  33653  evls1fldgencl  33657  irngss  33674  irngnzply1  33678  minplymindeg  33688  minplyirredlem  33690  irredminply  33696  algextdeglem2  33698  constrconj  33725  constrfiss  33731  1smat1  33781  submat1n  33782  lmatfval  33791  lmatcl  33793  mdetpmtr1  33800  madjusmdetlem4  33807  qtopt1  33812  qtophaus  33813  locfinref  33818  zarcls1  33846  zarclsiin  33848  zarmxt1  33857  zarcmplem  33858  rhmpreimacn  33862  ordtrest2NEWlem  33899  elzrhunit  33954  qqhcn  33968  qqhucn  33969  esumel  34024  esumsplit  34030  sigagenss2  34127  elsx  34171  sxbrsigalem0  34249  dya2icoseg  34255  eulerpartlemb  34346  eulerpartlemgvv  34354  iwrdsplit  34365  sseqfv2  34372  probfinmeasb  34406  dstrvprob  34450  dstfrvel  34452  ballotlemrv  34498  signstfvn  34547  signstfvp  34549  signstfveq0  34555  signsvtp  34561  signsvtn  34562  reprsuc  34593  reprpmtf1o  34604  lpadleft  34661  bnj1006  34937  bnj1018g  34940  bnj1018  34941  bnj1121  34962  bnj1398  35011  bnj1450  35027  bnj1501  35044  revpfxsfxrev  35084  swrdrevpfx  35085  pfxwlk  35092  revwlk  35093  swrdwlk  35095  subfacp1lem5  35152  ptpconn  35201  indispconn  35202  cvxsconn  35211  cvmseu  35244  cvmliftmolem2  35250  cvmliftlem7  35259  cvmliftlem10  35262  cvmliftlem13  35264  cvmlift2lem12  35282  satfv1lem  35330  satffunlem1lem2  35371  satffunlem2lem2  35374  satefvfmla1  35393  mrsubcv  35478  mrsubff  35480  mrsubrn  35481  mrsubccat  35486  elmrsubrn  35488  mrsubco  35489  mrsubvrs  35490  mvhf  35526  msubvrs  35528  mclsax  35537  r1peuqusdeg1  35611  linerflx1  36113  linerflx2  36115  fwddifnval  36127  elhf2  36139  neibastop2lem  36324  weiunpo  36429  weiunso  36430  icoreunrn  37323  relowlssretop  37327  sucneqond  37329  matunitlindflem2  37587  poimirlem4  37594  poimirlem20  37610  poimirlem30  37620  broucube  37624  opnmbllem0  37626  areacirclem2  37679  areacirclem4  37681  blssp  37726  sstotbnd2  37744  totbndbnd  37759  prdstotbnd  37764  cnpwstotbnd  37767  heiborlem9  37789  exidcl  37846  exidresid  37849  grpokerinj  37863  iscringd  37968  erimeq2  38642  prter3  38846  toycom  38937  islfld  39026  lshpsmreu  39073  ldualelvbase  39091  ldualssvscl  39122  lkreqN  39134  lkrlspeqN  39135  erng1lem  40952  erngdvlem4  40956  erng0g  40959  erng1r  40960  erngdvlem4-rN  40964  dva0g  40992  dia1dim2  41027  dia1dimid  41028  dia2dimlem5  41033  dvhelvbasei  41053  dvhvaddass  41062  tendoinvcl  41069  tendolinv  41070  tendorinv  41071  dvhgrp  41072  dvhlveclem  41073  cdlemn4  41163  lcfrlem12N  41519  lcfrlem15  41522  lcdvscl  41570  lcdlssvscl  41571  lcdvsass  41572  lcdvs0N  41581  mapdincl  41626  mapdin  41627  mapdlsmcl  41628  mapdcnvatN  41631  mapdpglem2  41638  mapdpglem12  41648  mapdpglem18  41654  mapdpglem21  41657  mapdpglem22  41658  mapdpglem28  41666  mapdpglem30  41667  hdmaprnlem3N  41815  hdmaprnlem3uN  41816  hdmaprnlem7N  41820  hdmaprnlem8N  41821  hdmaprnlem9N  41822  hdmaprnlem3eN  41823  hdmaprnlem16N  41827  hgmapdcl  41855  hgmapval1  41858  hgmaprnlem4N  41864  hdmapinvlem1  41883  fzadd2d  41937  aks6d1c2lem4  42086  sticksstones1  42105  sticksstones8  42112  sticksstones9  42113  sticksstones10  42114  sticksstones11  42115  sticksstones17  42122  sticksstones18  42123  aks6d1c6lem4  42132  rhmqusspan  42144  aks5lem2  42146  mhmcopsr  42519  evlsbagval  42536  evlsevl  42541  evlvvval  42543  evlvvvallem  42544  selvcllem2  42548  evlselv  42557  mhpind  42564  fltnltalem  42632  wepwsolem  43013  kercvrlsm  43054  dfacbasgrp  43079  onexomgt  43212  onexoegt  43215  onov0suclim  43245  cantnftermord  43291  cantnf2  43296  omcl2  43304  ofoaf  43326  ofoafo  43327  grurankcld  44205  grumnudlem  44257  grumnud  44258  inaex  44269  gruex  44270  dvconstbi  44306  cncmpmax  45004  iooabslt  45476  fmul01lt1lem2  45562  limciccioolb  45598  limcicciooub  45614  limsuppnfdlem  45678  climrescn  45725  climxrrelem  45726  climxrre  45727  liminflimsupxrre  45794  xlimmnfvlem2  45810  xlimpnfvlem2  45814  fsumcncf  45855  ioccncflimc  45862  icocncflimc  45866  cncfiooicclem1  45870  dvbdfbdioolem2  45906  dvnmul  45920  dvnprodlem1  45923  stoweidlem26  46003  stoweidlem34  46011  stoweidlem48  46025  stoweidlem59  46036  dirkercncflem3  46082  fourierdlem32  46116  fourierdlem41  46125  fourierdlem51  46134  fourierdlem63  46146  fourierdlem82  46165  fourierdlem85  46168  fourierdlem93  46176  fourierdlem111  46194  fourierdlem114  46197  etransclem35  46246  hspdifhsp  46593  opnvonmbllem1  46609  ovnovollem1  46633  mbfresmf  46716  smfaddlem1  46740  smfsuplem1  46788  smflimsuplem5  46801  setsidel  47338  setsnidel  47339  imasetpreimafvbijlemf  47363  prelspr  47448  upgrimpths  47870  gpgprismgr4cycllem9  48050  rngccatidALTV  48195  rhmsubcALTVlem3  48206  funcringcsetcALTV2lem3  48215  funcringcsetcALTV2lem8  48220  ringccatidALTV  48229  funcringcsetclem3ALTV  48238  funcringcsetclem8ALTV  48243  srhmsubcALTVlem1  48246  srhmsubcALTV  48248  lcosslsp  48362  nnolog2flm1  48518  glbprlem  48887  topdlat  48926  catprs  48934  iinfsubc  48973  iinfconstbaslem  48980  imaid  49042  fthcomf  49045  swapf2  49139  swapfiso  49150  swapciso  49151  cofuswapf2  49154  fuco22natlem  49204  oppcthinco  49273  oppcthinendcALT  49275  thinccisod  49288  termchommo  49318  termcid  49319  termcterm  49346  termcterm2  49347  diagciso  49372  diagcic  49373  mndtccatid  49412  grptcmon  49418  grptcepi  49419  2arwcat  49425  lanval2  49450  ranval2  49453  lanup  49463  ranup  49464