Theorem eleqtrrd 2841

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  3eltr4d  2853  rspc2vd  3958  disjxiun  5144  eldmressnsn  6043  elimdelov  7528  elovmpt3rab1  7692  fnwelem  8154  tfrlem13  8428  tz7.44-2  8445  omordi  8602  oneo  8617  omeulem2  8619  oeordi  8623  oeeui  8638  nnneo  8691  naddelim  8722  erref  8763  en1uniel  9067  omxpenlem  9111  unblem3  9327  dffi3  9468  ordtypelem10  9564  oismo  9577  cantnff  9711  cantnfp1lem3  9717  cantnflem1  9726  cnfcom  9737  r1ordg  9815  r1pwss  9821  rankwflemb  9830  r1elwf  9833  rankidb  9837  rankonidlem  9865  fseqenlem2  10062  dfac12lem1  10181  dfac12lem2  10182  pwsdompw  10240  ackbij2lem3  10277  ackbij2  10279  cfsmolem  10307  hsmexlem4  10466  ttukeylem3  10548  ttukeylem7  10552  iundom2g  10577  fpwwe2lem8  10675  canthwelem  10687  pwfseqlem4  10699  winalim2  10733  r1wunlim  10774  tskmid  10877  fzopth  13597  predfz  13689  fzoss2  13723  fz1fzo0m1  13746  fzo0addel  13753  fzo0addelr  13754  elfzoext  13757  fzosubel3  13761  elfzomin  13772  elfzonlteqm1  13776  fzoend  13792  fzoopth  13797  fzofzp1  13799  fzofzp1b  13800  peano2fzor  13809  zmodfzo  13930  seqf1olem2  14079  bcn2  14354  swrdccat2  14703  pfxccat1  14736  swrdswrd  14739  pfxccatin12  14767  splfv1  14789  revcl  14795  revlen  14796  revccat  14800  revrev  14801  repswpfx  14819  cshwidxmod  14837  revco  14869  limsupgre  15513  summolem2a  15747  fsumm1  15783  fsumcom2  15806  prodmolem2a  15966  fprodm1  15999  fprodcom2  16016  prmreclem4  16952  prmreclem5  16953  vdwapid1  17008  vdwlem5  17018  vdwlem8  17021  vdwnnlem2  17029  ramub1lem1  17059  ramub1lem2  17060  mrieqvlemd  17673  mreexd  17686  mreexexlemd  17688  catcocl  17729  catass  17730  moni  17783  epii  17790  inviso1  17813  episect  17832  invisoinvl  17837  catsubcat  17889  subccocl  17895  fullsubc  17900  funcco  17921  resf2nd  17945  funcres  17946  fthepi  17981  nati  18009  arwhoma  18098  catccatid  18159  resscatc  18162  catcisolem  18163  catcoppccl  18170  catcoppcclOLD  18171  catcfuccl  18172  catcfucclOLD  18173  estrreslem2  18193  funcestrcsetclem3  18197  funcestrcsetclem8  18202  equivestrcsetc  18207  funcsetcestrclem3  18211  funcsetcestrclem8  18217  xpcco  18238  xpcco2  18242  xpccatid  18243  prfcl  18258  catcxpccl  18262  catcxpcclOLD  18263  curf12  18283  curf1cl  18284  curf2  18285  curf2cl  18287  curfcl  18288  uncf2  18293  uncfcurf  18295  diag12  18300  diag2  18301  curf2ndf  18303  hofcl  18315  oppchofcl  18316  oyoncl  18326  yonedalem3a  18330  yonedalem4b  18332  yonedalem22  18334  yonedalem3b  18335  yonedalem3  18336  yonedainv  18337  yonffthlem  18338  latcl2  18493  latlem  18494  latjcom  18504  latmcom  18520  clatlem  18559  clatlubcl2  18561  clatglbcl2  18563  acsfiindd  18610  gsumpropd2lem  18704  sgrppropd  18756  mndpropd  18784  imasmnd  18800  frmdmnd  18884  frmdgsum  18887  grpsubpropd2  19076  imasgrp  19086  subg0  19162  0ghm  19260  resghm2  19263  ghmco  19266  pwsdiagghm  19274  ghmqusnsglem2  19311  ghmqusnsg  19312  ghmquskerlem2  19315  ghmquskerlem3  19316  ghmqusker  19317  psgnunilem1  19525  psgnunilem5  19526  psgnunilem2  19527  psgnunilem3  19528  sylow1lem4  19633  sylow1lem5  19634  efglem  19748  efgtf  19754  efginvrel2  19759  efginvrel1  19760  efgsdmi  19764  efgs1b  19768  efgsres  19770  efgsfo  19771  efgredleme  19775  efgredlemc  19777  efgredlem  19779  efgcpbllemb  19787  frgp0  19792  frgpadd  19795  frgpinv  19796  vrgpf  19800  vrgpinv  19801  frgpuplem  19804  frgpup1  19807  frgpup2  19808  frgpup3lem  19809  frgpnabllem1  19905  frgpnabllem2  19906  gsumval3  19939  dprdfid  20051  dprdsn  20070  dprd2da  20076  dpjidcl  20092  pgpfac1lem2  20109  pgpfaclem3  20117  ablsimpg1gend  20139  ablsimpgprmd  20149  rngpropd  20191  imasrng  20194  ringpropd  20301  imasring  20343  qusring2  20347  pwsco1rhm  20518  pwsco2rhm  20519  lringuplu  20560  subrgunit  20606  pwsdiagrhm  20623  rnghmsubcsetclem1  20647  zrinitorngc  20658  zrtermorngc  20659  zrzeroorngc  20660  rhmsubcsetclem1  20676  rhmsubcrngclem1  20682  zrtermoringc  20691  zrninitoringc  20692  srhmsubclem2  20694  srhmsubc  20696  cntzsdrg  20819  isabvd  20829  lmodprop2d  20938  islssd  20950  prdsvscacl  20983  prdslmodd  20984  islmhm2  21054  lmhmco  21059  lmhmplusg  21060  lmhmvsca  21061  lmhmpropd  21089  lsppreli  21106  ellspsn4  21143  lssacsex  21163  lspsnat  21164  lidlnsg  21275  qus2idrng  21300  qus1  21301  qusrhm  21303  rhmpreimaidl  21304  rhmqusnsg  21312  rngqiprngghmlem1  21314  rngqiprngfulem1  21338  irinitoringc  21507  nzerooringczr  21508  znf1o  21587  cssmre  21728  dsmmlss  21781  frlmsplit2  21810  frlmbas3  21813  frlmup1  21835  assapropd  21909  psr0cl  21989  psrnegcl  21991  psr1cl  21998  resspsrmul  22013  subrgpsr  22015  mvrf  22022  mplmon  22070  mplcoe1  22072  subrgasclcl  22108  mplind  22111  evlslem1  22123  subrgply1  22249  psrplusgpropd  22252  ply1coe  22317  cply1coe0bi  22321  lply1binomsc  22330  ply1fermltlchr  22331  evls1val  22339  evls1rhm  22341  evl1val  22348  evl1rhm  22351  pf1ind  22374  evl1scvarpw  22382  evls1fpws  22388  mhmcompl  22399  rhmply1  22405  matbas2i  22443  matplusg2  22448  matvsca2  22449  matsubgcell  22455  matvscacell  22457  mpomatmul  22467  mavmulval  22566  mavmulcl  22568  mavmulass  22570  mavmul0  22573  mavmumamul1  22576  m1detdiag  22618  cramerimplem2  22705  mat2pmatmul  22752  mat2pmatlin  22756  monmatcollpw  22800  pmatcollpwfi  22803  mply1topmatcl  22826  pm2mpghm  22837  pm2mpmhmlem2  22840  pm2mp  22846  chpmat1dlem  22856  chpmat1d  22857  chpdmatlem0  22858  chpscmat  22863  chpscmatgsumbin  22865  chpscmatgsummon  22866  chfacfscmulcl  22878  cpmadugsumlemB  22895  cpmadugsumlemC  22896  chcoeffeqlem  22906  cldmreon  23117  neiptopreu  23156  maxlp  23170  ordttopon  23216  ordtrest2lem  23226  cnprcl2  23274  lmcnp  23327  resthauslem  23386  hauscmplem  23429  1stcfb  23468  2ndcctbss  23478  2ndcomap  23481  dis2ndc  23483  loclly  23510  hausllycmp  23517  locfincmp  23549  dissnref  23551  kgeni  23560  kgenidm  23570  ptpjpre2  23603  xkoopn  23612  txopn  23625  ptpjopn  23635  ptcldmpt  23637  ptcls  23639  pthaus  23661  txkgen  23675  xkohaus  23676  xkopt  23678  txconn  23712  imastps  23744  kqid  23751  kqopn  23757  kqcld  23758  isr0  23760  indishmph  23821  pt1hmeo  23829  ptuncnv  23830  ptunhmeo  23831  t0kq  23841  filconn  23906  uzrest  23920  uffixsn  23948  fmfnfmlem2  23978  flimss2  23995  flimss1  23996  flimclslem  24007  flfcnp  24027  fclsfnflim  24050  uffclsflim  24054  fcfelbas  24059  alexsublem  24067  alexsub  24068  cnextcn  24090  cnextfres1  24091  cnextfres  24092  tmdgsum  24118  distgp  24122  indistgp  24123  symgtgp  24129  ghmcnp  24138  qustgpopn  24143  qustgplem  24144  qustgphaus  24146  prdstmdd  24147  prdstgpd  24148  tsmsid  24163  tsmssubm  24166  tsmsmhm  24169  tsmsadd  24170  tsmssplit  24175  utop2nei  24274  utop3cls  24275  neipcfilu  24320  cnextucn  24327  ucnextcn  24328  blpnfctr  24461  lpbl  24531  met2ndci  24550  tmsxps  24564  metcnpi  24572  metcnpi2  24573  metcnpi3  24574  metustid  24582  metustsym  24583  metustexhalf  24584  subgngp  24663  ngptgp  24664  sranlm  24720  nlmvscn  24723  nrginvrcn  24728  lssnlm  24737  nghmcn  24781  iccntr  24856  icccmplem2  24858  msdcn  24876  cncfmptc  24951  cncfmptid  24952  cncfmpt2f  24954  icoopnst  24982  iocopnst  24983  nmoleub2lem3  25161  nmoleub3  25165  nmhmcn  25166  ipcn  25293  cfilfcls  25321  caucfil  25330  equivcau  25347  caubl  25355  flimcfil  25361  cmssmscld  25397  rrxdstprj1  25456  minveclem3b  25475  minveclem4  25479  mulcncf  25493  ovolicc2lem3  25567  ovolicc2lem4  25568  opnmbllem  25649  vitalilem2  25657  mbfsup  25712  mbfinf  25713  mbfi1fseqlem4  25767  limccnp  25940  limccnp2  25941  dvreslem  25958  dvres2lem  25959  dvidlem  25964  dvcnp2  25969  dvcnp2OLD  25970  dvcn  25971  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvcmul  25995  dvcof  26000  dvcnvlem  26028  dvef  26032  rollelem  26041  dvlip2  26048  dvivthlem1  26061  dvivth  26063  lhop2  26068  lhop  26069  dvcnvrelem1  26070  dvcnvrelem2  26071  dvcnvre  26072  ply1rem  26219  fta1blem  26224  plycpn  26345  plyrem  26361  tayl0  26417  dvtaylp  26426  dvntaylp  26427  dvntaylp0  26428  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmdvlem3  26459  psercn  26484  pserdv  26487  abelth  26499  efabl  26606  efopnlem1  26712  loglesqrt  26818  relogbf  26848  efrlim  27026  efrlimOLD  27027  dchrghm  27314  dchrptlem3  27324  nodenselem5  27747  nosupres  27766  noinfres  27781  sltlpss  27959  precsexlem11  28255  noseq0  28310  noseqp1  28311  noseqrdgfn  28326  noseqrdgsuc  28328  tgbtwntriv2  28509  tgbtwnne  28512  ercgrg  28539  tgidinside  28593  tgbtwnconn1  28597  tglnne  28650  tglnne0  28662  tglnpt2  28663  tglineneq  28666  ncolncol  28668  coltr3  28670  mirln  28698  mirln2  28699  mirconn  28700  krippenlem  28712  footexALT  28740  footexlem1  28741  footexlem2  28742  colperpexlem3  28754  mideulem2  28756  opphllem  28757  oppne3  28765  opphllem1  28769  opphllem2  28770  opphllem4  28772  oppperpex  28775  opphl  28776  hlpasch  28778  hpgerlem  28787  colhp  28792  midbtwn  28801  lmieu  28806  lmiisolem  28818  sacgr  28853  f1otrg  28893  f1otrge  28894  ebtwntg  29011  ecgrtg  29012  eengtrkg  29015  eengtrkge  29016  upgr1eop  29146  usgredg3  29247  uspgr1eop  29278  usgr1eop  29281  vtxdun  29513  vtxdfiun  29514  1loopgruspgr  29532  1loopgrvd2  29535  1hevtxdg1  29538  1egrvtxdg1  29541  1egrvtxdg0  29543  umgr2v2e  29557  wlkres  29702  wlkp1lem4  29708  wlkp1  29713  wwlksm1edg  29910  wwlksnext  29922  wwlksnextproplem3  29940  clwwlkel  30074  1wlkdlem2  30166  trlsegvdeg  30255  eupth2lem3lem1  30256  eupth2lem3lem2  30257  extwwlkfab  30380  numclwlk2lem2f  30405  spansnid  31591  elspansn4  31601  fnpreimac  32687  ccatf1  32917  ccatws1f1olast  32921  swrdrn2  32923  swrdrn3  32924  swrdf1  32925  splfv3  32927  pwrssmgc  32974  pfxchn  32983  chnind  32984  chnub  32985  chnlt  32986  wrdpmtrlast  33095  psgnfzto1stlem  33102  cycpmfv1  33115  cycpmfv2  33116  cycpmco2lem2  33129  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2  33135  cyc3co2  33142  cycpmrn  33145  submarchi  33175  subrdom  33268  fracfld  33289  imaslmod  33360  quslmod  33365  quslmhm  33366  nsgqusf1olem2  33421  lmhmqusker  33424  rhmquskerlem  33432  idlinsubrg  33438  drngidl  33440  rhmpreimaprmidl  33458  qsidomlem2  33460  mxidlprm  33477  opprmxidlabs  33494  qsdrngilem  33501  qsdrngi  33502  qsdrnglem2  33503  idlsrg0g  33513  pidufd  33550  dfufd2lem  33556  fply1  33563  evl1fpws  33569  ressply1sub  33574  ply1asclunit  33578  r1plmhm  33609  drgextlsp  33622  matdim  33642  ply1degltdimlem  33649  lindsunlem  33651  qusdimsum  33655  fedgmullem1  33656  fedgmullem2  33657  fedgmul  33658  extdg1id  33690  evls1fldgencl  33694  irngss  33701  irngnzply1  33705  minplymindeg  33715  minplyirredlem  33717  irredminply  33721  algextdeglem2  33723  constrconj  33749  1smat1  33764  submat1n  33765  lmatfval  33774  lmatcl  33776  mdetpmtr1  33783  madjusmdetlem4  33790  qtopt1  33795  qtophaus  33796  locfinref  33801  zarcls1  33829  zarclsiin  33831  zarmxt1  33840  zarcmplem  33841  rhmpreimacn  33845  ordtrest2NEWlem  33882  elzrhunit  33939  qqhcn  33953  qqhucn  33954  esumel  34027  esumsplit  34033  sigagenss2  34130  elsx  34174  sxbrsigalem0  34252  dya2icoseg  34258  eulerpartlemb  34349  eulerpartlemgvv  34357  iwrdsplit  34368  sseqfv2  34375  probfinmeasb  34409  dstrvprob  34452  dstfrvel  34454  ballotlemrv  34500  signstfvn  34562  signstfvp  34564  signstfveq0  34570  signsvtp  34576  signsvtn  34577  reprsuc  34608  reprpmtf1o  34619  lpadleft  34676  bnj1006  34952  bnj1018g  34955  bnj1018  34956  bnj1121  34977  bnj1398  35026  bnj1450  35042  bnj1501  35059  revpfxsfxrev  35099  swrdrevpfx  35100  pfxwlk  35107  revwlk  35108  swrdwlk  35110  subfacp1lem5  35168  ptpconn  35217  indispconn  35218  cvxsconn  35227  cvmseu  35260  cvmliftmolem2  35266  cvmliftlem7  35275  cvmliftlem10  35278  cvmliftlem13  35280  cvmlift2lem12  35298  satfv1lem  35346  satffunlem1lem2  35387  satffunlem2lem2  35390  satefvfmla1  35409  mrsubcv  35494  mrsubff  35496  mrsubrn  35497  mrsubccat  35502  elmrsubrn  35504  mrsubco  35505  mrsubvrs  35506  mvhf  35542  msubvrs  35544  mclsax  35553  r1peuqusdeg1  35627  linerflx1  36130  linerflx2  36132  fwddifnval  36144  elhf2  36156  neibastop2lem  36342  weiunpo  36447  weiunso  36448  icoreunrn  37341  relowlssretop  37345  sucneqond  37347  matunitlindflem2  37603  poimirlem4  37610  poimirlem20  37626  poimirlem30  37636  broucube  37640  opnmbllem0  37642  areacirclem2  37695  areacirclem4  37697  blssp  37742  sstotbnd2  37760  totbndbnd  37775  prdstotbnd  37780  cnpwstotbnd  37783  heiborlem9  37805  exidcl  37862  exidresid  37865  grpokerinj  37879  iscringd  37984  erimeq2  38659  prter3  38863  toycom  38954  islfld  39043  lshpsmreu  39090  ldualelvbase  39108  ldualssvscl  39139  lkreqN  39151  lkrlspeqN  39152  erng1lem  40969  erngdvlem4  40973  erng0g  40976  erng1r  40977  erngdvlem4-rN  40981  dva0g  41009  dia1dim2  41044  dia1dimid  41045  dia2dimlem5  41050  dvhelvbasei  41070  dvhvaddass  41079  tendoinvcl  41086  tendolinv  41087  tendorinv  41088  dvhgrp  41089  dvhlveclem  41090  cdlemn4  41180  lcfrlem12N  41536  lcfrlem15  41539  lcdvscl  41587  lcdlssvscl  41588  lcdvsass  41589  lcdvs0N  41598  mapdincl  41643  mapdin  41644  mapdlsmcl  41645  mapdcnvatN  41648  mapdpglem2  41655  mapdpglem12  41665  mapdpglem18  41671  mapdpglem21  41674  mapdpglem22  41675  mapdpglem28  41683  mapdpglem30  41684  hdmaprnlem3N  41832  hdmaprnlem3uN  41833  hdmaprnlem7N  41837  hdmaprnlem8N  41838  hdmaprnlem9N  41839  hdmaprnlem3eN  41840  hdmaprnlem16N  41844  hgmapdcl  41872  hgmapval1  41875  hgmaprnlem4N  41881  hdmapinvlem1  41900  fzadd2d  41959  aks6d1c2lem4  42108  sticksstones1  42127  sticksstones8  42134  sticksstones9  42135  sticksstones10  42136  sticksstones11  42137  sticksstones17  42144  sticksstones18  42145  aks6d1c6lem4  42154  rhmqusspan  42166  aks5lem2  42168  fnsnbt  42249  mhmcopsr  42535  evlsbagval  42552  evlsevl  42557  evlvvval  42559  evlvvvallem  42560  selvcllem2  42564  evlselv  42573  mhpind  42580  fltnltalem  42648  wepwsolem  43030  kercvrlsm  43071  dfacbasgrp  43096  onexomgt  43229  onexoegt  43232  onov0suclim  43263  cantnftermord  43309  cantnf2  43314  omcl2  43322  ofoaf  43344  ofoafo  43345  grurankcld  44228  grumnudlem  44280  grumnud  44281  inaex  44292  gruex  44293  dvconstbi  44329  cncmpmax  44969  iooabslt  45451  fmul01lt1lem2  45540  limciccioolb  45576  limcicciooub  45592  limsuppnfdlem  45656  climrescn  45703  climxrrelem  45704  climxrre  45705  liminflimsupxrre  45772  xlimmnfvlem2  45788  xlimpnfvlem2  45792  fsumcncf  45833  ioccncflimc  45840  icocncflimc  45844  cncfiooicclem1  45848  dvbdfbdioolem2  45884  dvnmul  45898  dvnprodlem1  45901  stoweidlem26  45981  stoweidlem34  45989  stoweidlem48  46003  stoweidlem59  46014  dirkercncflem3  46060  fourierdlem32  46094  fourierdlem41  46103  fourierdlem51  46112  fourierdlem63  46124  fourierdlem82  46143  fourierdlem85  46146  fourierdlem93  46154  fourierdlem111  46172  fourierdlem114  46175  etransclem35  46224  hspdifhsp  46571  opnvonmbllem1  46587  ovnovollem1  46611  mbfresmf  46694  smfaddlem1  46718  smfsuplem1  46766  smflimsuplem5  46779  setsidel  47300  setsnidel  47301  imasetpreimafvbijlemf  47325  prelspr  47410  rngccatidALTV  48115  rhmsubcALTVlem3  48126  funcringcsetcALTV2lem3  48135  funcringcsetcALTV2lem8  48140  ringccatidALTV  48149  funcringcsetclem3ALTV  48158  funcringcsetclem8ALTV  48163  srhmsubcALTVlem1  48166  srhmsubcALTV  48168  lcosslsp  48283  nnolog2flm1  48439  glbprlem  48761  topdlat  48792  catprs  48799  thinccisod  48849  mndtccatid  48895  grptcmon  48901  grptcepi  48902