Theorem eleqtrrd 2835

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2809

This theorem is referenced by:  3eltr4d  2847  rspc2vd  3944  disjxiun  5145  eldmressnsn  6024  elimdelov  7508  elovmpt3rab1  7670  fnwelem  8122  tfrlem13  8396  tz7.44-2  8413  omordi  8572  oneo  8587  omeulem2  8589  oeordi  8593  oeeui  8608  nnneo  8660  naddelim  8691  erref  8729  en1uniel  9034  en1unielOLD  9035  omxpenlem  9079  unblem3  9303  dffi3  9432  ordtypelem10  9528  oismo  9541  cantnff  9675  cantnfp1lem3  9681  cantnflem1  9690  cnfcom  9701  r1ordg  9779  r1pwss  9785  rankwflemb  9794  r1elwf  9797  rankidb  9801  rankonidlem  9829  fseqenlem2  10026  dfac12lem1  10144  dfac12lem2  10145  pwsdompw  10205  ackbij2lem3  10242  ackbij2  10244  cfsmolem  10271  hsmexlem4  10430  ttukeylem3  10512  ttukeylem7  10516  iundom2g  10541  fpwwe2lem8  10639  canthwelem  10651  pwfseqlem4  10663  winalim2  10697  r1wunlim  10738  tskmid  10841  fzopth  13545  predfz  13633  fzoss2  13667  fz1fzo0m1  13687  fzo0addel  13693  fzo0addelr  13694  fzosubel3  13700  elfzomin  13711  elfzonlteqm1  13715  fzoend  13730  fzofzp1  13736  fzofzp1b  13737  peano2fzor  13746  zmodfzo  13866  seqf1olem2  14015  bcn2  14286  swrdccat2  14626  pfxccat1  14659  swrdswrd  14662  pfxccatin12  14690  splfv1  14712  revcl  14718  revlen  14719  revccat  14723  revrev  14724  repswpfx  14742  cshwidxmod  14760  revco  14792  limsupgre  15432  summolem2a  15668  fsumm1  15704  fsumcom2  15727  prodmolem2a  15885  fprodm1  15918  fprodcom2  15935  prmreclem4  16859  prmreclem5  16860  vdwapid1  16915  vdwlem5  16925  vdwlem8  16928  vdwnnlem2  16936  ramub1lem1  16966  ramub1lem2  16967  mrieqvlemd  17580  mreexd  17593  mreexexlemd  17595  catcocl  17636  catass  17637  moni  17690  epii  17697  inviso1  17720  episect  17739  invisoinvl  17744  catsubcat  17796  subccocl  17802  fullsubc  17807  funcco  17828  resf2nd  17852  funcres  17853  fthepi  17888  nati  17916  arwhoma  18005  catccatid  18066  resscatc  18069  catcisolem  18070  catcoppccl  18077  catcoppcclOLD  18078  catcfuccl  18079  catcfucclOLD  18080  estrreslem2  18100  funcestrcsetclem3  18104  funcestrcsetclem8  18109  equivestrcsetc  18114  funcsetcestrclem3  18118  funcsetcestrclem8  18124  xpcco  18145  xpcco2  18149  xpccatid  18150  prfcl  18165  catcxpccl  18169  catcxpcclOLD  18170  curf12  18190  curf1cl  18191  curf2  18192  curf2cl  18194  curfcl  18195  uncf2  18200  uncfcurf  18202  diag12  18207  diag2  18208  curf2ndf  18210  hofcl  18222  oppchofcl  18223  oyoncl  18233  yonedalem3a  18237  yonedalem4b  18239  yonedalem22  18241  yonedalem3b  18242  yonedalem3  18243  yonedainv  18244  yonffthlem  18245  latcl2  18399  latlem  18400  latjcom  18410  latmcom  18426  clatlem  18465  clatlubcl2  18467  clatglbcl2  18469  acsfiindd  18516  gsumpropd2lem  18610  sgrppropd  18662  mndpropd  18690  imasmnd  18703  frmdmnd  18782  frmdgsum  18785  grpsubpropd2  18972  imasgrp  18982  subg0  19055  0ghm  19151  resghm2  19154  ghmco  19157  pwsdiagghm  19165  psgnunilem1  19409  psgnunilem5  19410  psgnunilem2  19411  psgnunilem3  19412  sylow1lem4  19517  sylow1lem5  19518  efglem  19632  efgtf  19638  efginvrel2  19643  efginvrel1  19644  efgsdmi  19648  efgs1b  19652  efgsres  19654  efgsfo  19655  efgredleme  19659  efgredlemc  19661  efgredlem  19663  efgcpbllemb  19671  frgp0  19676  frgpadd  19679  frgpinv  19680  vrgpf  19684  vrgpinv  19685  frgpuplem  19688  frgpup1  19691  frgpup2  19692  frgpup3lem  19693  frgpnabllem1  19789  frgpnabllem2  19790  gsumval3  19823  dprdfid  19935  dprdsn  19954  dprd2da  19960  dpjidcl  19976  pgpfac1lem2  19993  pgpfaclem3  20001  ablsimpg1gend  20023  ablsimpgprmd  20033  rngpropd  20075  imasrng  20078  ringpropd  20183  imasring  20225  qusring2  20229  pwsco1rhm  20400  pwsco2rhm  20401  lringuplu  20440  subrgunit  20488  pwsdiagrhm  20505  rnghmsubcsetclem1  20523  zrinitorngc  20534  zrtermorngc  20535  zrzeroorngc  20536  rhmsubcsetclem1  20552  rhmsubcrngclem1  20558  zrtermoringc  20567  zrninitoringc  20568  srhmsubclem2  20570  srhmsubc  20572  cntzsdrg  20649  isabvd  20659  lmodprop2d  20766  islssd  20778  prdsvscacl  20811  prdslmodd  20812  islmhm2  20882  lmhmco  20887  lmhmplusg  20888  lmhmvsca  20889  lmhmpropd  20917  lsppreli  20934  lspsnel4  20971  lssacsex  20991  lspsnat  20992  qus1  21111  qusrhm  21113  qus2idrng  21133  rngqiprngghmlem1  21135  rngqiprngfulem1  21159  irinitoringc  21339  nzerooringczr  21340  znf1o  21417  cssmre  21556  dsmmlss  21609  frlmsplit2  21638  frlmbas3  21641  frlmup1  21663  assapropd  21736  psr0cl  21824  psrnegcl  21826  psr1cl  21833  resspsrmul  21848  subrgpsr  21850  mvrf  21855  mplmon  21901  mplcoe1  21903  subrgasclcl  21939  mplind  21942  evlslem1  21956  subrgply1  22075  psrplusgpropd  22078  ply1coe  22140  cply1coe0bi  22144  lply1binomsc  22151  evls1val  22159  evls1rhm  22161  evl1val  22168  evl1rhm  22171  pf1ind  22194  evl1scvarpw  22202  matbas2i  22244  matplusg2  22249  matvsca2  22250  matsubgcell  22256  matvscacell  22258  mpomatmul  22268  mavmulval  22367  mavmulcl  22369  mavmulass  22371  mavmul0  22374  mavmumamul1  22377  m1detdiag  22419  cramerimplem2  22506  mat2pmatmul  22553  mat2pmatlin  22557  monmatcollpw  22601  pmatcollpwfi  22604  mply1topmatcl  22627  pm2mpghm  22638  pm2mpmhmlem2  22641  pm2mp  22647  chpmat1dlem  22657  chpmat1d  22658  chpdmatlem0  22659  chpscmat  22664  chpscmatgsumbin  22666  chpscmatgsummon  22667  chfacfscmulcl  22679  cpmadugsumlemB  22696  cpmadugsumlemC  22697  chcoeffeqlem  22707  cldmreon  22918  neiptopreu  22957  maxlp  22971  ordttopon  23017  ordtrest2lem  23027  cnprcl2  23075  lmcnp  23128  resthauslem  23187  hauscmplem  23230  1stcfb  23269  2ndcctbss  23279  2ndcomap  23282  dis2ndc  23284  loclly  23311  hausllycmp  23318  locfincmp  23350  dissnref  23352  kgeni  23361  kgenidm  23371  ptpjpre2  23404  xkoopn  23413  txopn  23426  ptpjopn  23436  ptcldmpt  23438  ptcls  23440  pthaus  23462  txkgen  23476  xkohaus  23477  xkopt  23479  txconn  23513  imastps  23545  kqid  23552  kqopn  23558  kqcld  23559  isr0  23561  indishmph  23622  pt1hmeo  23630  ptuncnv  23631  ptunhmeo  23632  t0kq  23642  filconn  23707  uzrest  23721  uffixsn  23749  fmfnfmlem2  23779  flimss2  23796  flimss1  23797  flimclslem  23808  flfcnp  23828  fclsfnflim  23851  uffclsflim  23855  fcfelbas  23860  alexsublem  23868  alexsub  23869  cnextcn  23891  cnextfres1  23892  cnextfres  23893  tmdgsum  23919  distgp  23923  indistgp  23924  symgtgp  23930  ghmcnp  23939  qustgpopn  23944  qustgplem  23945  qustgphaus  23947  prdstmdd  23948  prdstgpd  23949  tsmsid  23964  tsmssubm  23967  tsmsmhm  23970  tsmsadd  23971  tsmssplit  23976  utop2nei  24075  utop3cls  24076  neipcfilu  24121  cnextucn  24128  ucnextcn  24129  blpnfctr  24262  lpbl  24332  met2ndci  24351  tmsxps  24365  metcnpi  24373  metcnpi2  24374  metcnpi3  24375  metustid  24383  metustsym  24384  metustexhalf  24385  subgngp  24464  ngptgp  24465  sranlm  24521  nlmvscn  24524  nrginvrcn  24529  lssnlm  24538  nghmcn  24582  iccntr  24657  icccmplem2  24659  msdcn  24677  cncfmptc  24752  cncfmptid  24753  cncfmpt2f  24755  icoopnst  24783  iocopnst  24784  nmoleub2lem3  24962  nmoleub3  24966  nmhmcn  24967  ipcn  25094  cfilfcls  25122  caucfil  25131  equivcau  25148  caubl  25156  flimcfil  25162  cmssmscld  25198  rrxdstprj1  25257  minveclem3b  25276  minveclem4  25280  mulcncf  25294  ovolicc2lem3  25368  ovolicc2lem4  25369  opnmbllem  25450  vitalilem2  25458  mbfsup  25513  mbfinf  25514  mbfi1fseqlem4  25568  limccnp  25740  limccnp2  25741  dvreslem  25758  dvres2lem  25759  dvidlem  25764  dvcnp2  25769  dvcnp2OLD  25770  dvcn  25771  dvaddbr  25788  dvmulbr  25789  dvmulbrOLD  25790  dvcmul  25795  dvcof  25800  dvcnvlem  25828  dvef  25832  rollelem  25841  dvlip2  25848  dvivthlem1  25861  dvivth  25863  lhop2  25868  lhop  25869  dvcnvrelem1  25870  dvcnvrelem2  25871  dvcnvre  25872  ply1rem  26019  fta1blem  26024  plycpn  26141  plyrem  26157  tayl0  26213  dvtaylp  26221  dvntaylp  26222  dvntaylp0  26223  taylthlem1  26224  taylthlem2  26225  ulmdvlem3  26253  psercn  26278  pserdv  26281  abelth  26293  efabl  26399  efopnlem1  26504  loglesqrt  26607  relogbf  26637  efrlim  26815  dchrghm  27102  dchrptlem3  27112  nodenselem5  27534  nosupres  27553  noinfres  27568  sltlpss  27746  precsexlem11  28028  tgbtwntriv2  28171  tgbtwnne  28174  ercgrg  28201  tgidinside  28255  tgbtwnconn1  28259  tglnne  28312  tglnne0  28324  tglnpt2  28325  tglineneq  28328  ncolncol  28330  coltr3  28332  mirln  28360  mirln2  28361  mirconn  28362  krippenlem  28374  footexALT  28402  footexlem1  28403  footexlem2  28404  colperpexlem3  28416  mideulem2  28418  opphllem  28419  oppne3  28427  opphllem1  28431  opphllem2  28432  opphllem4  28434  oppperpex  28437  opphl  28438  hlpasch  28440  hpgerlem  28449  colhp  28454  midbtwn  28463  lmieu  28468  lmiisolem  28480  sacgr  28515  f1otrg  28555  f1otrge  28556  ebtwntg  28673  ecgrtg  28674  eengtrkg  28677  eengtrkge  28678  upgr1eop  28808  usgredg3  28906  uspgr1eop  28937  usgr1eop  28940  vtxdun  29171  vtxdfiun  29172  1loopgruspgr  29190  1loopgrvd2  29193  1hevtxdg1  29196  1egrvtxdg1  29199  1egrvtxdg0  29201  umgr2v2e  29215  wlkres  29360  wlkp1lem4  29366  wlkp1  29371  wwlksm1edg  29568  wwlksnext  29580  wwlksnextproplem3  29598  clwwlkel  29732  1wlkdlem2  29824  trlsegvdeg  29913  eupth2lem3lem1  29914  eupth2lem3lem2  29915  extwwlkfab  30038  numclwlk2lem2f  30063  spansnid  31249  elspansn4  31259  fnpreimac  32329  ccatf1  32548  swrdrn2  32551  swrdrn3  32552  swrdf1  32553  splfv3  32555  pwrssmgc  32603  psgnfzto1stlem  32695  cycpmfv1  32708  cycpmfv2  32709  cycpmco2lem2  32722  cycpmco2lem4  32724  cycpmco2lem5  32725  cycpmco2lem6  32726  cycpmco2  32728  cyc3co2  32735  cycpmrn  32738  submarchi  32768  imaslmod  32904  quslmod  32909  quslmhm  32910  nsgqusf1olem2  32965  ghmquskerlem2  32970  ghmquskerlem3  32971  ghmqusker  32972  lmhmqusker  32974  rhmpreimaidl  32977  rhmquskerlem  32983  idlinsubrg  32989  drngidl  32991  lidlnsg  33004  rhmpreimaprmidl  33010  qsidomlem2  33012  mxidlprm  33026  opprmxidlabs  33041  qsdrngilem  33048  qsdrngi  33049  qsdrnglem2  33050  idlsrg0g  33060  fply1  33077  evls1fpws  33086  ply1asclunit  33094  ressply1sub  33099  ply1fermltlchr  33102  r1plmhm  33121  drgextlsp  33134  matdim  33154  ply1degltdimlem  33161  lindsunlem  33163  qusdimsum  33167  fedgmullem1  33168  fedgmullem2  33169  fedgmul  33170  extdg1id  33196  evls1fldgencl  33199  irngss  33206  irngnzply1  33210  minplyirredlem  33224  algextdeglem2  33229  1smat1  33248  submat1n  33249  lmatfval  33258  lmatcl  33260  mdetpmtr1  33267  madjusmdetlem4  33274  qtopt1  33279  qtophaus  33280  locfinref  33285  zarcls1  33313  zarclsiin  33315  zarmxt1  33324  zarcmplem  33325  rhmpreimacn  33329  ordtrest2NEWlem  33366  elzrhunit  33423  qqhcn  33435  qqhucn  33436  esumel  33509  esumsplit  33515  sigagenss2  33612  elsx  33656  sxbrsigalem0  33734  dya2icoseg  33740  eulerpartlemb  33831  eulerpartlemgvv  33839  iwrdsplit  33850  sseqfv2  33857  probfinmeasb  33891  dstrvprob  33934  dstfrvel  33936  ballotlemrv  33982  signstfvn  34044  signstfvp  34046  signstfveq0  34052  signsvtp  34058  signsvtn  34059  reprsuc  34091  reprpmtf1o  34102  lpadleft  34159  bnj1006  34435  bnj1018g  34438  bnj1018  34439  bnj1121  34460  bnj1398  34509  bnj1450  34525  bnj1501  34542  revpfxsfxrev  34570  swrdrevpfx  34571  pfxwlk  34578  revwlk  34579  swrdwlk  34581  subfacp1lem5  34639  ptpconn  34688  indispconn  34689  cvxsconn  34698  cvmseu  34731  cvmliftmolem2  34737  cvmliftlem7  34746  cvmliftlem10  34749  cvmliftlem13  34751  cvmlift2lem12  34769  satfv1lem  34817  satffunlem1lem2  34858  satffunlem2lem2  34861  satefvfmla1  34880  mrsubcv  34965  mrsubff  34967  mrsubrn  34968  mrsubccat  34973  elmrsubrn  34975  mrsubco  34976  mrsubvrs  34977  mvhf  35013  msubvrs  35015  mclsax  35024  linerflx1  35591  linerflx2  35593  fwddifnval  35605  elhf2  35617  neibastop2lem  35709  icoreunrn  36704  relowlssretop  36708  sucneqond  36710  matunitlindflem2  36949  poimirlem4  36956  poimirlem20  36972  poimirlem30  36982  broucube  36986  opnmbllem0  36988  areacirclem2  37041  areacirclem4  37043  blssp  37088  sstotbnd2  37106  totbndbnd  37121  prdstotbnd  37126  cnpwstotbnd  37129  heiborlem9  37151  exidcl  37208  exidresid  37211  grpokerinj  37225  iscringd  37330  erimeq2  38012  prter3  38216  toycom  38307  islfld  38396  lshpsmreu  38443  ldualelvbase  38461  ldualssvscl  38492  lkreqN  38504  lkrlspeqN  38505  erng1lem  40322  erngdvlem4  40326  erng0g  40329  erng1r  40330  erngdvlem4-rN  40334  dva0g  40362  dia1dim2  40397  dia1dimid  40398  dia2dimlem5  40403  dvhelvbasei  40423  dvhvaddass  40432  tendoinvcl  40439  tendolinv  40440  tendorinv  40441  dvhgrp  40442  dvhlveclem  40443  cdlemn4  40533  lcfrlem12N  40889  lcfrlem15  40892  lcdvscl  40940  lcdlssvscl  40941  lcdvsass  40942  lcdvs0N  40951  mapdincl  40996  mapdin  40997  mapdlsmcl  40998  mapdcnvatN  41001  mapdpglem2  41008  mapdpglem12  41018  mapdpglem18  41024  mapdpglem21  41027  mapdpglem22  41028  mapdpglem28  41036  mapdpglem30  41037  hdmaprnlem3N  41185  hdmaprnlem3uN  41186  hdmaprnlem7N  41190  hdmaprnlem8N  41191  hdmaprnlem9N  41192  hdmaprnlem3eN  41193  hdmaprnlem16N  41197  hgmapdcl  41225  hgmapval1  41228  hgmaprnlem4N  41234  hdmapinvlem1  41253  fzadd2d  41310  sticksstones1  41429  sticksstones8  41436  sticksstones9  41437  sticksstones10  41438  sticksstones11  41439  sticksstones17  41446  sticksstones18  41447  fnsnbt  41518  mhmcompl  41583  evlsbagval  41601  evlsevl  41606  evlvvval  41608  evlvvvallem  41609  selvcllem2  41613  evlselv  41622  mhpind  41629  fltnltalem  41867  wepwsolem  42247  kercvrlsm  42288  dfacbasgrp  42313  onexomgt  42453  onexoegt  42456  onov0suclim  42487  cantnftermord  42533  cantnf2  42538  omcl2  42546  ofoaf  42568  ofoafo  42569  imo72b2lem0  43380  grurankcld  43455  grumnudlem  43507  grumnud  43508  inaex  43519  gruex  43520  dvconstbi  43556  cncmpmax  44179  iooabslt  44671  fmul01lt1lem2  44760  limciccioolb  44796  limcicciooub  44812  limsuppnfdlem  44876  climrescn  44923  climxrrelem  44924  climxrre  44925  liminflimsupxrre  44992  xlimmnfvlem2  45008  xlimpnfvlem2  45012  fsumcncf  45053  ioccncflimc  45060  icocncflimc  45064  cncfiooicclem1  45068  dvbdfbdioolem2  45104  dvnmul  45118  stoweidlem26  45201  stoweidlem34  45209  stoweidlem48  45223  stoweidlem59  45234  dirkercncflem3  45280  fourierdlem32  45314  fourierdlem41  45323  fourierdlem51  45332  fourierdlem63  45344  fourierdlem82  45363  fourierdlem85  45366  fourierdlem93  45374  fourierdlem111  45392  fourierdlem114  45395  etransclem35  45444  hspdifhsp  45791  opnvonmbllem1  45807  ovnovollem1  45831  mbfresmf  45914  smfaddlem1  45938  smfsuplem1  45986  smflimsuplem5  45999  fzoopth  46494  setsidel  46503  setsnidel  46504  imasetpreimafvbijlemf  46528  prelspr  46613  rngccatidALTV  47109  rhmsubcALTVlem3  47120  funcringcsetcALTV2lem3  47129  funcringcsetcALTV2lem8  47134  ringccatidALTV  47143  funcringcsetclem3ALTV  47152  funcringcsetclem8ALTV  47157  srhmsubcALTVlem1  47160  srhmsubcALTV  47162  lcosslsp  47281  nnolog2flm1  47438  glbprlem  47760  topdlat  47791  catprs  47793  mndtccatid  47875  grptcmon  47878  grptcepi  47879