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  3898  disjxiun  5096  eldmressnsn  5984  fnsnbg  7112  elimdelov  7456  elovmpt3rab1  7620  fnwelem  8075  tfrlem13  8323  tz7.44-2  8340  omordi  8495  oneo  8510  omeulem2  8512  oeordi  8517  oeeui  8532  nnneo  8585  naddelim  8616  erref  8658  en1uniel  8970  omxpenlem  9010  unblem3  9198  dffi3  9338  ordtypelem10  9436  oismo  9449  cantnff  9587  cantnfp1lem3  9593  cantnflem1  9602  cnfcom  9613  r1ordg  9694  r1pwss  9700  rankwflemb  9709  r1elwf  9712  rankidb  9716  rankonidlem  9744  fseqenlem2  9939  dfac12lem1  10058  dfac12lem2  10059  pwsdompw  10117  ackbij2lem3  10154  ackbij2  10156  cfsmolem  10184  hsmexlem4  10343  ttukeylem3  10425  ttukeylem7  10429  iundom2g  10454  fpwwe2lem8  10553  canthwelem  10565  pwfseqlem4  10577  winalim2  10611  r1wunlim  10652  tskmid  10755  fzopth  13481  predfz  13573  fzoss2  13607  fz1fzo0m1  13630  fzo0addel  13638  fzo0addelr  13639  elfzoext  13642  fzosubel3  13646  elfzomin  13657  elfzonlteqm1  13661  fzoend  13677  fzoopth  13682  fzofzp1  13684  fzofzp1b  13685  peano2fzor  13695  zmodfzo  13818  seqf1olem2  13969  bcn2  14246  swrdccat2  14597  pfxccat1  14629  swrdswrd  14632  pfxccatin12  14660  splfv1  14682  revcl  14688  revlen  14689  revccat  14693  revrev  14694  repswpfx  14712  cshwidxmod  14730  revco  14761  limsupgre  15408  summolem2a  15642  fsumm1  15678  fsumcom2  15701  prodmolem2a  15861  fprodm1  15894  fprodcom2  15911  prmreclem4  16851  prmreclem5  16852  vdwapid1  16907  vdwlem5  16917  vdwlem8  16920  vdwnnlem2  16928  ramub1lem1  16958  ramub1lem2  16959  mrieqvlemd  17556  mreexd  17569  mreexexlemd  17571  catcocl  17612  catass  17613  moni  17664  epii  17671  inviso1  17694  episect  17713  invisoinvl  17718  catsubcat  17767  subccocl  17773  fullsubc  17778  funcco  17799  resf2nd  17823  funcres  17824  fthepi  17858  nati  17886  arwhoma  17973  catccatid  18034  resscatc  18037  catcisolem  18038  catcoppccl  18045  catcfuccl  18046  estrreslem2  18065  funcestrcsetclem3  18069  funcestrcsetclem8  18074  equivestrcsetc  18079  funcsetcestrclem3  18083  funcsetcestrclem8  18089  xpcco  18110  xpcco2  18114  xpccatid  18115  prfcl  18130  catcxpccl  18134  curf12  18154  curf1cl  18155  curf2  18156  curf2cl  18158  curfcl  18159  uncf2  18164  uncfcurf  18166  diag12  18171  diag2  18172  curf2ndf  18174  hofcl  18186  oppchofcl  18187  oyoncl  18197  yonedalem3a  18201  yonedalem4b  18203  yonedalem22  18205  yonedalem3b  18206  yonedalem3  18207  yonedainv  18208  yonffthlem  18209  latcl2  18363  latlem  18364  latjcom  18374  latmcom  18390  clatlem  18429  clatlubcl2  18431  clatglbcl2  18433  acsfiindd  18480  pfxchn  18537  chnind  18548  chnub  18549  chnlt  18550  chnccat  18553  chnrev  18554  gsumpropd2lem  18608  sgrppropd  18660  mndpropd  18688  imasmnd  18704  frmdmnd  18788  frmdgsum  18791  grpsubpropd2  18980  imasgrp  18990  subg0  19066  0ghm  19163  resghm2  19166  ghmco  19169  pwsdiagghm  19177  ghmqusnsglem2  19214  ghmqusnsg  19215  ghmquskerlem2  19218  ghmquskerlem3  19219  ghmqusker  19220  psgnunilem1  19426  psgnunilem5  19427  psgnunilem2  19428  psgnunilem3  19429  sylow1lem4  19534  sylow1lem5  19535  efglem  19649  efgtf  19655  efginvrel2  19660  efginvrel1  19661  efgsdmi  19665  efgs1b  19669  efgsres  19671  efgsfo  19672  efgredleme  19676  efgredlemc  19678  efgredlem  19680  efgcpbllemb  19688  frgp0  19693  frgpadd  19696  frgpinv  19697  vrgpf  19701  vrgpinv  19702  frgpuplem  19705  frgpup1  19708  frgpup2  19709  frgpup3lem  19710  frgpnabllem1  19806  frgpnabllem2  19807  gsumval3  19840  dprdfid  19952  dprdsn  19971  dprd2da  19977  dpjidcl  19993  pgpfac1lem2  20010  pgpfaclem3  20018  ablsimpg1gend  20040  ablsimpgprmd  20050  rngpropd  20113  imasrng  20116  ringpropd  20227  imasring  20270  qusring2  20274  pwsco1rhm  20439  pwsco2rhm  20440  lringuplu  20481  subrgunit  20527  pwsdiagrhm  20544  rnghmsubcsetclem1  20568  zrinitorngc  20579  zrtermorngc  20580  zrzeroorngc  20581  rhmsubcsetclem1  20597  rhmsubcrngclem1  20603  zrtermoringc  20612  zrninitoringc  20613  srhmsubclem2  20615  srhmsubc  20617  cntzsdrg  20739  isabvd  20749  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  21652  dsmmlss  21703  frlmsplit2  21732  frlmbas3  21735  frlmup1  21757  assapropd  21831  psr0cl  21912  psrnegcl  21914  psr1cl  21920  resspsrmul  21935  subrgpsr  21937  mvrf  21944  mplmon  21994  mplcoe1  21996  subrgasclcl  22026  mplind  22029  evlslem1  22041  subrgply1  22177  psrplusgpropd  22180  ply1coe  22246  cply1coe0bi  22250  lply1binomsc  22259  ply1fermltlchr  22260  evls1val  22268  evls1rhm  22270  evl1val  22277  evl1rhm  22280  pf1ind  22303  evl1scvarpw  22311  evls1fpws  22317  mhmcompl  22328  rhmply1  22334  matbas2i  22370  matplusg2  22375  matvsca2  22376  matsubgcell  22382  matvscacell  22384  mpomatmul  22394  mavmulval  22493  mavmulcl  22495  mavmulass  22497  mavmul0  22500  mavmumamul1  22503  m1detdiag  22545  cramerimplem2  22632  mat2pmatmul  22679  mat2pmatlin  22683  monmatcollpw  22727  pmatcollpwfi  22730  mply1topmatcl  22753  pm2mpghm  22764  pm2mpmhmlem2  22767  pm2mp  22773  chpmat1dlem  22783  chpmat1d  22784  chpdmatlem0  22785  chpscmat  22790  chpscmatgsumbin  22792  chpscmatgsummon  22793  chfacfscmulcl  22805  cpmadugsumlemB  22822  cpmadugsumlemC  22823  chcoeffeqlem  22833  cldmreon  23042  neiptopreu  23081  maxlp  23095  ordttopon  23141  ordtrest2lem  23151  cnprcl2  23199  lmcnp  23252  resthauslem  23311  hauscmplem  23354  1stcfb  23393  2ndcctbss  23403  2ndcomap  23406  dis2ndc  23408  loclly  23435  hausllycmp  23442  locfincmp  23474  dissnref  23476  kgeni  23485  kgenidm  23495  ptpjpre2  23528  xkoopn  23537  txopn  23550  ptpjopn  23560  ptcldmpt  23562  ptcls  23564  pthaus  23586  txkgen  23600  xkohaus  23601  xkopt  23603  txconn  23637  imastps  23669  kqid  23676  kqopn  23682  kqcld  23683  isr0  23685  indishmph  23746  pt1hmeo  23754  ptuncnv  23755  ptunhmeo  23756  t0kq  23766  filconn  23831  uzrest  23845  uffixsn  23873  fmfnfmlem2  23903  flimss2  23920  flimss1  23921  flimclslem  23932  flfcnp  23952  fclsfnflim  23975  uffclsflim  23979  fcfelbas  23984  alexsublem  23992  alexsub  23993  cnextcn  24015  cnextfres1  24016  cnextfres  24017  tmdgsum  24043  distgp  24047  indistgp  24048  symgtgp  24054  ghmcnp  24063  qustgpopn  24068  qustgplem  24069  qustgphaus  24071  prdstmdd  24072  prdstgpd  24073  tsmsid  24088  tsmssubm  24091  tsmsmhm  24094  tsmsadd  24095  tsmssplit  24100  utop2nei  24198  utop3cls  24199  neipcfilu  24243  cnextucn  24250  ucnextcn  24251  blpnfctr  24384  lpbl  24451  met2ndci  24470  tmsxps  24484  metcnpi  24492  metcnpi2  24493  metcnpi3  24494  metustid  24502  metustsym  24503  metustexhalf  24504  subgngp  24583  ngptgp  24584  sranlm  24632  nlmvscn  24635  nrginvrcn  24640  lssnlm  24649  nghmcn  24693  iccntr  24770  icccmplem2  24772  msdcn  24790  cncfmptc  24865  cncfmptid  24866  cncfmpt2f  24868  icoopnst  24896  iocopnst  24897  nmoleub2lem3  25075  nmoleub3  25079  nmhmcn  25080  ipcn  25206  cfilfcls  25234  caucfil  25243  equivcau  25260  caubl  25268  flimcfil  25274  cmssmscld  25310  rrxdstprj1  25369  minveclem3b  25388  minveclem4  25392  mulcncf  25406  ovolicc2lem3  25480  ovolicc2lem4  25481  opnmbllem  25562  vitalilem2  25570  mbfsup  25625  mbfinf  25626  mbfi1fseqlem4  25679  limccnp  25852  limccnp2  25853  dvreslem  25870  dvres2lem  25871  dvidlem  25876  dvcnp2  25881  dvcnp2OLD  25882  dvcn  25883  dvaddbr  25900  dvmulbr  25901  dvmulbrOLD  25902  dvcmul  25907  dvcof  25912  dvcnvlem  25940  dvef  25944  rollelem  25953  dvlip2  25960  dvivthlem1  25973  dvivth  25975  lhop2  25980  lhop  25981  dvcnvrelem1  25982  dvcnvrelem2  25983  dvcnvre  25984  ply1rem  26131  fta1blem  26136  plycpn  26257  plyrem  26273  tayl0  26329  dvtaylp  26338  dvntaylp  26339  dvntaylp0  26340  taylthlem1  26341  taylthlem2  26342  taylthlem2OLD  26343  ulmdvlem3  26371  psercn  26396  pserdv  26399  abelth  26411  efabl  26519  efopnlem1  26625  loglesqrt  26731  relogbf  26761  efrlim  26939  efrlimOLD  26940  dchrghm  27227  dchrptlem3  27237  nodenselem5  27660  nosupres  27679  noinfres  27694  ltslpss  27908  precsexlem11  28217  noseq0  28290  noseqp1  28291  noseqrdgfn  28306  noseqrdgsuc  28308  tgbtwntriv2  28563  tgbtwnne  28566  ercgrg  28593  tgidinside  28647  tgbtwnconn1  28651  tglnne  28704  tglnne0  28716  tglnpt2  28717  tglineneq  28720  ncolncol  28722  coltr3  28724  mirln  28752  mirln2  28753  mirconn  28754  krippenlem  28766  footexALT  28794  footexlem1  28795  footexlem2  28796  colperpexlem3  28808  mideulem2  28810  opphllem  28811  oppne3  28819  opphllem1  28823  opphllem2  28824  opphllem4  28826  oppperpex  28829  opphl  28830  hlpasch  28832  hpgerlem  28841  colhp  28846  midbtwn  28855  lmieu  28860  lmiisolem  28872  sacgr  28907  f1otrg  28947  f1otrge  28948  ebtwntg  29059  ecgrtg  29060  eengtrkg  29063  eengtrkge  29064  upgr1eop  29192  usgredg3  29293  uspgr1eop  29324  usgr1eop  29327  vtxdun  29559  vtxdfiun  29560  1loopgruspgr  29578  1loopgrvd2  29581  1hevtxdg1  29584  1egrvtxdg1  29587  1egrvtxdg0  29589  umgr2v2e  29603  wlkres  29746  wlkp1lem4  29752  wlkp1  29757  cyclnumvtx  29877  wwlksm1edg  29958  wwlksnext  29970  wwlksnextproplem3  29988  clwwlkel  30125  1wlkdlem2  30217  trlsegvdeg  30306  eupth2lem3lem1  30307  eupth2lem3lem2  30308  extwwlkfab  30431  numclwlk2lem2f  30456  spansnid  31642  elspansn4  31652  fnpreimac  32751  ccatf1  33033  ccatws1f1olast  33036  swrdrn2  33038  swrdrn3  33039  swrdf1  33040  splfv3  33042  pwrssmgc  33084  wrdpmtrlast  33177  psgnfzto1stlem  33184  cycpmfv1  33197  cycpmfv2  33198  cycpmco2lem2  33211  cycpmco2lem4  33213  cycpmco2lem5  33214  cycpmco2lem6  33215  cycpmco2  33217  cyc3co2  33224  cycpmrn  33227  submarchi  33270  subrdom  33369  fracfld  33392  imaslmod  33436  quslmod  33441  quslmhm  33442  nsgqusf1olem2  33497  lmhmqusker  33500  rhmquskerlem  33508  idlinsubrg  33514  drngidl  33516  rhmpreimaprmidl  33534  qsidomlem2  33536  mxidlprm  33553  opprmxidlabs  33570  qsdrngilem  33577  qsdrngi  33578  qsdrnglem2  33579  idlsrg0g  33589  pidufd  33626  dfufd2lem  33632  fply1  33641  evl1fpws  33647  ressply1evls1  33648  ressply1sub  33653  ply1asclunit  33657  r1plmhm  33693  extvfvcl  33703  evlextv  33709  mplvrpmga  33712  issply  33721  esplympl  33727  esplyind  33733  drgextlsp  33752  matdim  33774  ply1degltdimlem  33781  lindsunlem  33783  qusdimsum  33787  fedgmullem1  33788  fedgmullem2  33789  fedgmul  33790  extdg1id  33825  evls1fldgencl  33829  irngss  33846  irngnzply1  33850  extdgfialglem1  33851  extdgfialglem2  33852  minplymindeg  33867  minplyirredlem  33869  irredminply  33875  algextdeglem2  33877  constrconj  33904  constrfiss  33910  1smat1  33963  submat1n  33964  lmatfval  33973  lmatcl  33975  mdetpmtr1  33982  madjusmdetlem4  33989  qtopt1  33994  qtophaus  33995  locfinref  34000  zarcls1  34028  zarclsiin  34030  zarmxt1  34039  zarcmplem  34040  rhmpreimacn  34044  ordtrest2NEWlem  34081  elzrhunit  34136  qqhcn  34150  qqhucn  34151  esumel  34206  esumsplit  34212  sigagenss2  34309  elsx  34353  sxbrsigalem0  34430  dya2icoseg  34436  eulerpartlemb  34527  eulerpartlemgvv  34535  iwrdsplit  34546  sseqfv2  34553  probfinmeasb  34587  dstrvprob  34631  dstfrvel  34633  ballotlemrv  34679  signstfvn  34728  signstfvp  34730  signstfveq0  34736  signsvtp  34742  signsvtn  34743  reprsuc  34774  reprpmtf1o  34785  lpadleft  34842  bnj1006  35118  bnj1018g  35121  bnj1018  35122  bnj1121  35143  bnj1398  35192  bnj1450  35208  bnj1501  35225  revpfxsfxrev  35312  swrdrevpfx  35313  pfxwlk  35320  revwlk  35321  swrdwlk  35323  subfacp1lem5  35380  ptpconn  35429  indispconn  35430  cvxsconn  35439  cvmseu  35472  cvmliftmolem2  35478  cvmliftlem7  35487  cvmliftlem10  35490  cvmliftlem13  35492  cvmlift2lem12  35510  satfv1lem  35558  satffunlem1lem2  35599  satffunlem2lem2  35602  satefvfmla1  35621  mrsubcv  35706  mrsubff  35708  mrsubrn  35709  mrsubccat  35714  elmrsubrn  35716  mrsubco  35717  mrsubvrs  35718  mvhf  35754  msubvrs  35756  mclsax  35765  r1peuqusdeg1  35839  linerflx1  36345  linerflx2  36347  fwddifnval  36359  elhf2  36371  neibastop2lem  36556  weiunpo  36661  weiunso  36662  icoreunrn  37566  relowlssretop  37570  sucneqond  37572  matunitlindflem2  37820  poimirlem4  37827  poimirlem20  37843  poimirlem30  37853  broucube  37857  opnmbllem0  37859  areacirclem2  37912  areacirclem4  37914  blssp  37959  sstotbnd2  37977  totbndbnd  37992  prdstotbnd  37997  cnpwstotbnd  38000  heiborlem9  38022  exidcl  38079  exidresid  38082  grpokerinj  38096  iscringd  38201  erimeq2  38966  prter3  39210  toycom  39301  islfld  39390  lshpsmreu  39437  ldualelvbase  39455  ldualssvscl  39486  lkreqN  39498  lkrlspeqN  39499  erng1lem  41315  erngdvlem4  41319  erng0g  41322  erng1r  41323  erngdvlem4-rN  41327  dva0g  41355  dia1dim2  41390  dia1dimid  41391  dia2dimlem5  41396  dvhelvbasei  41416  dvhvaddass  41425  tendoinvcl  41432  tendolinv  41433  tendorinv  41434  dvhgrp  41435  dvhlveclem  41436  cdlemn4  41526  lcfrlem12N  41882  lcfrlem15  41885  lcdvscl  41933  lcdlssvscl  41934  lcdvsass  41935  lcdvs0N  41944  mapdincl  41989  mapdin  41990  mapdlsmcl  41991  mapdcnvatN  41994  mapdpglem2  42001  mapdpglem12  42011  mapdpglem18  42017  mapdpglem21  42020  mapdpglem22  42021  mapdpglem28  42029  mapdpglem30  42030  hdmaprnlem3N  42178  hdmaprnlem3uN  42179  hdmaprnlem7N  42183  hdmaprnlem8N  42184  hdmaprnlem9N  42185  hdmaprnlem3eN  42186  hdmaprnlem16N  42190  hgmapdcl  42218  hgmapval1  42221  hgmaprnlem4N  42227  hdmapinvlem1  42246  fzadd2d  42300  aks6d1c2lem4  42449  sticksstones1  42468  sticksstones8  42475  sticksstones9  42476  sticksstones10  42477  sticksstones11  42478  sticksstones17  42485  sticksstones18  42486  aks6d1c6lem4  42495  rhmqusspan  42507  aks5lem2  42509  mhmcopsr  42869  evlsbagval  42879  evlsevl  42884  evlvvval  42885  evlvvvallem  42886  selvcllem2  42888  evlselv  42897  mhpind  42904  fltnltalem  42972  wepwsolem  43351  kercvrlsm  43392  dfacbasgrp  43417  onexomgt  43550  onexoegt  43553  onov0suclim  43583  cantnftermord  43629  cantnf2  43634  omcl2  43642  ofoaf  43664  ofoafo  43665  grurankcld  44541  grumnudlem  44593  grumnud  44594  inaex  44605  gruex  44606  dvconstbi  44642  cncmpmax  45344  iooabslt  45812  fmul01lt1lem2  45898  limciccioolb  45934  limcicciooub  45948  limsuppnfdlem  46012  climrescn  46059  climxrrelem  46060  climxrre  46061  liminflimsupxrre  46128  xlimmnfvlem2  46144  xlimpnfvlem2  46148  fsumcncf  46189  ioccncflimc  46196  icocncflimc  46200  cncfiooicclem1  46204  dvbdfbdioolem2  46240  dvnmul  46254  dvnprodlem1  46257  stoweidlem26  46337  stoweidlem34  46345  stoweidlem48  46359  stoweidlem59  46370  dirkercncflem3  46416  fourierdlem32  46450  fourierdlem41  46459  fourierdlem51  46468  fourierdlem63  46480  fourierdlem82  46499  fourierdlem85  46502  fourierdlem93  46510  fourierdlem111  46528  fourierdlem114  46531  etransclem35  46580  hspdifhsp  46927  opnvonmbllem1  46943  ovnovollem1  46967  mbfresmf  47050  smfaddlem1  47074  smfsuplem1  47122  smflimsuplem5  47135  chnerlem2  47194  setsidel  47689  setsnidel  47690  imasetpreimafvbijlemf  47714  prelspr  47799  upgrimpths  48222  gpgprismgr4cycllem9  48416  rngccatidALTV  48585  rhmsubcALTVlem3  48596  funcringcsetcALTV2lem3  48605  funcringcsetcALTV2lem8  48610  ringccatidALTV  48619  funcringcsetclem3ALTV  48628  funcringcsetclem8ALTV  48633  srhmsubcALTVlem1  48636  srhmsubcALTV  48638  lcosslsp  48751  nnolog2flm1  48903  ffvbr  49168  glbprlem  49277  topdlat  49316  catprs  49323  iinfsubc  49370  iinfconstbaslem  49377  imaid  49466  fthcomf  49469  uptr2  49533  natoppf2  49542  natoppfb  49543  swapf2  49586  swapfiso  49597  swapciso  49598  oppc1stflem  49599  cofuswapf2  49607  fuco22natlem  49657  fucoppcffth  49723  oppcthinco  49751  oppcthinendcALT  49753  thinccisod  49766  termco  49793  termchommo  49797  termcid  49798  termcterm  49825  termcterm2  49826  diagciso  49851  diagcic  49852  funcsn  49853  uobeqterm  49858  mndtccatid  49899  grptcmon  49905  grptcepi  49906  2arwcat  49912  lanval2  49939  ranval2  49942  lanup  49953  ranup  49954  lmddu  49979