Theorem eleqtrrd 2831

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  3eltr4d  2843  rspc2vd  3910  disjxiun  5104  eldmressnsn  5995  fnsnbg  7138  elimdelov  7485  elovmpt3rab1  7649  fnwelem  8110  tfrlem13  8358  tz7.44-2  8375  omordi  8530  oneo  8545  omeulem2  8547  oeordi  8551  oeeui  8566  nnneo  8619  naddelim  8650  erref  8691  en1uniel  9000  omxpenlem  9042  unblem3  9241  dffi3  9382  ordtypelem10  9480  oismo  9493  cantnff  9627  cantnfp1lem3  9633  cantnflem1  9642  cnfcom  9653  r1ordg  9731  r1pwss  9737  rankwflemb  9746  r1elwf  9749  rankidb  9753  rankonidlem  9781  fseqenlem2  9978  dfac12lem1  10097  dfac12lem2  10098  pwsdompw  10156  ackbij2lem3  10193  ackbij2  10195  cfsmolem  10223  hsmexlem4  10382  ttukeylem3  10464  ttukeylem7  10468  iundom2g  10493  fpwwe2lem8  10591  canthwelem  10603  pwfseqlem4  10615  winalim2  10649  r1wunlim  10690  tskmid  10793  fzopth  13522  predfz  13614  fzoss2  13648  fz1fzo0m1  13671  fzo0addel  13679  fzo0addelr  13680  elfzoext  13683  fzosubel3  13687  elfzomin  13698  elfzonlteqm1  13702  fzoend  13718  fzoopth  13723  fzofzp1  13725  fzofzp1b  13726  peano2fzor  13735  zmodfzo  13856  seqf1olem2  14007  bcn2  14284  swrdccat2  14634  pfxccat1  14667  swrdswrd  14670  pfxccatin12  14698  splfv1  14720  revcl  14726  revlen  14727  revccat  14731  revrev  14732  repswpfx  14750  cshwidxmod  14768  revco  14800  limsupgre  15447  summolem2a  15681  fsumm1  15717  fsumcom2  15740  prodmolem2a  15900  fprodm1  15933  fprodcom2  15950  prmreclem4  16890  prmreclem5  16891  vdwapid1  16946  vdwlem5  16956  vdwlem8  16959  vdwnnlem2  16967  ramub1lem1  16997  ramub1lem2  16998  mrieqvlemd  17590  mreexd  17603  mreexexlemd  17605  catcocl  17646  catass  17647  moni  17698  epii  17705  inviso1  17728  episect  17747  invisoinvl  17752  catsubcat  17801  subccocl  17807  fullsubc  17812  funcco  17833  resf2nd  17857  funcres  17858  fthepi  17892  nati  17920  arwhoma  18007  catccatid  18068  resscatc  18071  catcisolem  18072  catcoppccl  18079  catcfuccl  18080  estrreslem2  18099  funcestrcsetclem3  18103  funcestrcsetclem8  18108  equivestrcsetc  18113  funcsetcestrclem3  18117  funcsetcestrclem8  18123  xpcco  18144  xpcco2  18148  xpccatid  18149  prfcl  18164  catcxpccl  18168  curf12  18188  curf1cl  18189  curf2  18190  curf2cl  18192  curfcl  18193  uncf2  18198  uncfcurf  18200  diag12  18205  diag2  18206  curf2ndf  18208  hofcl  18220  oppchofcl  18221  oyoncl  18231  yonedalem3a  18235  yonedalem4b  18237  yonedalem22  18239  yonedalem3b  18240  yonedalem3  18241  yonedainv  18242  yonffthlem  18243  latcl2  18395  latlem  18396  latjcom  18406  latmcom  18422  clatlem  18461  clatlubcl2  18463  clatglbcl2  18465  acsfiindd  18512  gsumpropd2lem  18606  sgrppropd  18658  mndpropd  18686  imasmnd  18702  frmdmnd  18786  frmdgsum  18789  grpsubpropd2  18978  imasgrp  18988  subg0  19064  0ghm  19162  resghm2  19165  ghmco  19168  pwsdiagghm  19176  ghmqusnsglem2  19213  ghmqusnsg  19214  ghmquskerlem2  19217  ghmquskerlem3  19218  ghmqusker  19219  psgnunilem1  19423  psgnunilem5  19424  psgnunilem2  19425  psgnunilem3  19426  sylow1lem4  19531  sylow1lem5  19532  efglem  19646  efgtf  19652  efginvrel2  19657  efginvrel1  19658  efgsdmi  19662  efgs1b  19666  efgsres  19668  efgsfo  19669  efgredleme  19673  efgredlemc  19675  efgredlem  19677  efgcpbllemb  19685  frgp0  19690  frgpadd  19693  frgpinv  19694  vrgpf  19698  vrgpinv  19699  frgpuplem  19702  frgpup1  19705  frgpup2  19706  frgpup3lem  19707  frgpnabllem1  19803  frgpnabllem2  19804  gsumval3  19837  dprdfid  19949  dprdsn  19968  dprd2da  19974  dpjidcl  19990  pgpfac1lem2  20007  pgpfaclem3  20015  ablsimpg1gend  20037  ablsimpgprmd  20047  rngpropd  20083  imasrng  20086  ringpropd  20197  imasring  20239  qusring2  20243  pwsco1rhm  20411  pwsco2rhm  20412  lringuplu  20453  subrgunit  20499  pwsdiagrhm  20516  rnghmsubcsetclem1  20540  zrinitorngc  20551  zrtermorngc  20552  zrzeroorngc  20553  rhmsubcsetclem1  20569  rhmsubcrngclem1  20575  zrtermoringc  20584  zrninitoringc  20585  srhmsubclem2  20587  srhmsubc  20589  cntzsdrg  20711  isabvd  20721  lmodprop2d  20830  islssd  20841  prdsvscacl  20874  prdslmodd  20875  islmhm2  20945  lmhmco  20950  lmhmplusg  20951  lmhmvsca  20952  lmhmpropd  20980  lsppreli  20997  ellspsn4  21034  lssacsex  21054  lspsnat  21055  lidlnsg  21158  qus2idrng  21183  qus1  21184  qusrhm  21186  rhmpreimaidl  21187  rhmqusnsg  21195  rngqiprngghmlem1  21197  rngqiprngfulem1  21221  irinitoringc  21389  nzerooringczr  21390  znf1o  21461  cssmre  21602  dsmmlss  21653  frlmsplit2  21682  frlmbas3  21685  frlmup1  21707  assapropd  21781  psr0cl  21861  psrnegcl  21863  psr1cl  21870  resspsrmul  21885  subrgpsr  21887  mvrf  21894  mplmon  21942  mplcoe1  21944  subrgasclcl  21974  mplind  21977  evlslem1  21989  subrgply1  22117  psrplusgpropd  22120  ply1coe  22185  cply1coe0bi  22189  lply1binomsc  22198  ply1fermltlchr  22199  evls1val  22207  evls1rhm  22209  evl1val  22216  evl1rhm  22219  pf1ind  22242  evl1scvarpw  22250  evls1fpws  22256  mhmcompl  22267  rhmply1  22273  matbas2i  22309  matplusg2  22314  matvsca2  22315  matsubgcell  22321  matvscacell  22323  mpomatmul  22333  mavmulval  22432  mavmulcl  22434  mavmulass  22436  mavmul0  22439  mavmumamul1  22442  m1detdiag  22484  cramerimplem2  22571  mat2pmatmul  22618  mat2pmatlin  22622  monmatcollpw  22666  pmatcollpwfi  22669  mply1topmatcl  22692  pm2mpghm  22703  pm2mpmhmlem2  22706  pm2mp  22712  chpmat1dlem  22722  chpmat1d  22723  chpdmatlem0  22724  chpscmat  22729  chpscmatgsumbin  22731  chpscmatgsummon  22732  chfacfscmulcl  22744  cpmadugsumlemB  22761  cpmadugsumlemC  22762  chcoeffeqlem  22772  cldmreon  22981  neiptopreu  23020  maxlp  23034  ordttopon  23080  ordtrest2lem  23090  cnprcl2  23138  lmcnp  23191  resthauslem  23250  hauscmplem  23293  1stcfb  23332  2ndcctbss  23342  2ndcomap  23345  dis2ndc  23347  loclly  23374  hausllycmp  23381  locfincmp  23413  dissnref  23415  kgeni  23424  kgenidm  23434  ptpjpre2  23467  xkoopn  23476  txopn  23489  ptpjopn  23499  ptcldmpt  23501  ptcls  23503  pthaus  23525  txkgen  23539  xkohaus  23540  xkopt  23542  txconn  23576  imastps  23608  kqid  23615  kqopn  23621  kqcld  23622  isr0  23624  indishmph  23685  pt1hmeo  23693  ptuncnv  23694  ptunhmeo  23695  t0kq  23705  filconn  23770  uzrest  23784  uffixsn  23812  fmfnfmlem2  23842  flimss2  23859  flimss1  23860  flimclslem  23871  flfcnp  23891  fclsfnflim  23914  uffclsflim  23918  fcfelbas  23923  alexsublem  23931  alexsub  23932  cnextcn  23954  cnextfres1  23955  cnextfres  23956  tmdgsum  23982  distgp  23986  indistgp  23987  symgtgp  23993  ghmcnp  24002  qustgpopn  24007  qustgplem  24008  qustgphaus  24010  prdstmdd  24011  prdstgpd  24012  tsmsid  24027  tsmssubm  24030  tsmsmhm  24033  tsmsadd  24034  tsmssplit  24039  utop2nei  24138  utop3cls  24139  neipcfilu  24183  cnextucn  24190  ucnextcn  24191  blpnfctr  24324  lpbl  24391  met2ndci  24410  tmsxps  24424  metcnpi  24432  metcnpi2  24433  metcnpi3  24434  metustid  24442  metustsym  24443  metustexhalf  24444  subgngp  24523  ngptgp  24524  sranlm  24572  nlmvscn  24575  nrginvrcn  24580  lssnlm  24589  nghmcn  24633  iccntr  24710  icccmplem2  24712  msdcn  24730  cncfmptc  24805  cncfmptid  24806  cncfmpt2f  24808  icoopnst  24836  iocopnst  24837  nmoleub2lem3  25015  nmoleub3  25019  nmhmcn  25020  ipcn  25146  cfilfcls  25174  caucfil  25183  equivcau  25200  caubl  25208  flimcfil  25214  cmssmscld  25250  rrxdstprj1  25309  minveclem3b  25328  minveclem4  25332  mulcncf  25346  ovolicc2lem3  25420  ovolicc2lem4  25421  opnmbllem  25502  vitalilem2  25510  mbfsup  25565  mbfinf  25566  mbfi1fseqlem4  25619  limccnp  25792  limccnp2  25793  dvreslem  25810  dvres2lem  25811  dvidlem  25816  dvcnp2  25821  dvcnp2OLD  25822  dvcn  25823  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvcmul  25847  dvcof  25852  dvcnvlem  25880  dvef  25884  rollelem  25893  dvlip2  25900  dvivthlem1  25913  dvivth  25915  lhop2  25920  lhop  25921  dvcnvrelem1  25922  dvcnvrelem2  25923  dvcnvre  25924  ply1rem  26071  fta1blem  26076  plycpn  26197  plyrem  26213  tayl0  26269  dvtaylp  26278  dvntaylp  26279  dvntaylp0  26280  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulmdvlem3  26311  psercn  26336  pserdv  26339  abelth  26351  efabl  26459  efopnlem1  26565  loglesqrt  26671  relogbf  26701  efrlim  26879  efrlimOLD  26880  dchrghm  27167  dchrptlem3  27177  nodenselem5  27600  nosupres  27619  noinfres  27634  sltlpss  27819  precsexlem11  28119  noseq0  28184  noseqp1  28185  noseqrdgfn  28200  noseqrdgsuc  28202  tgbtwntriv2  28414  tgbtwnne  28417  ercgrg  28444  tgidinside  28498  tgbtwnconn1  28502  tglnne  28555  tglnne0  28567  tglnpt2  28568  tglineneq  28571  ncolncol  28573  coltr3  28575  mirln  28603  mirln2  28604  mirconn  28605  krippenlem  28617  footexALT  28645  footexlem1  28646  footexlem2  28647  colperpexlem3  28659  mideulem2  28661  opphllem  28662  oppne3  28670  opphllem1  28674  opphllem2  28675  opphllem4  28677  oppperpex  28680  opphl  28681  hlpasch  28683  hpgerlem  28692  colhp  28697  midbtwn  28706  lmieu  28711  lmiisolem  28723  sacgr  28758  f1otrg  28798  f1otrge  28799  ebtwntg  28909  ecgrtg  28910  eengtrkg  28913  eengtrkge  28914  upgr1eop  29042  usgredg3  29143  uspgr1eop  29174  usgr1eop  29177  vtxdun  29409  vtxdfiun  29410  1loopgruspgr  29428  1loopgrvd2  29431  1hevtxdg1  29434  1egrvtxdg1  29437  1egrvtxdg0  29439  umgr2v2e  29453  wlkres  29598  wlkp1lem4  29604  wlkp1  29609  cyclnumvtx  29730  wwlksm1edg  29811  wwlksnext  29823  wwlksnextproplem3  29841  clwwlkel  29975  1wlkdlem2  30067  trlsegvdeg  30156  eupth2lem3lem1  30157  eupth2lem3lem2  30158  extwwlkfab  30281  numclwlk2lem2f  30306  spansnid  31492  elspansn4  31502  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  33140  subrdom  33235  fracfld  33258  imaslmod  33324  quslmod  33329  quslmhm  33330  nsgqusf1olem2  33385  lmhmqusker  33388  rhmquskerlem  33396  idlinsubrg  33402  drngidl  33404  rhmpreimaprmidl  33422  qsidomlem2  33424  mxidlprm  33441  opprmxidlabs  33458  qsdrngilem  33465  qsdrngi  33466  qsdrnglem2  33467  idlsrg0g  33477  pidufd  33514  dfufd2lem  33520  fply1  33527  evl1fpws  33533  ressply1evls1  33534  ressply1sub  33539  ply1asclunit  33543  r1plmhm  33575  drgextlsp  33589  matdim  33611  ply1degltdimlem  33618  lindsunlem  33620  qusdimsum  33624  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  extdg1id  33661  evls1fldgencl  33665  irngss  33682  irngnzply1  33686  minplymindeg  33698  minplyirredlem  33700  irredminply  33706  algextdeglem2  33708  constrconj  33735  constrfiss  33741  1smat1  33794  submat1n  33795  lmatfval  33804  lmatcl  33806  mdetpmtr1  33813  madjusmdetlem4  33820  qtopt1  33825  qtophaus  33826  locfinref  33831  zarcls1  33859  zarclsiin  33861  zarmxt1  33870  zarcmplem  33871  rhmpreimacn  33875  ordtrest2NEWlem  33912  elzrhunit  33967  qqhcn  33981  qqhucn  33982  esumel  34037  esumsplit  34043  sigagenss2  34140  elsx  34184  sxbrsigalem0  34262  dya2icoseg  34268  eulerpartlemb  34359  eulerpartlemgvv  34367  iwrdsplit  34378  sseqfv2  34385  probfinmeasb  34419  dstrvprob  34463  dstfrvel  34465  ballotlemrv  34511  signstfvn  34560  signstfvp  34562  signstfveq0  34568  signsvtp  34574  signsvtn  34575  reprsuc  34606  reprpmtf1o  34617  lpadleft  34674  bnj1006  34950  bnj1018g  34953  bnj1018  34954  bnj1121  34975  bnj1398  35024  bnj1450  35040  bnj1501  35057  revpfxsfxrev  35103  swrdrevpfx  35104  pfxwlk  35111  revwlk  35112  swrdwlk  35114  subfacp1lem5  35171  ptpconn  35220  indispconn  35221  cvxsconn  35230  cvmseu  35263  cvmliftmolem2  35269  cvmliftlem7  35278  cvmliftlem10  35281  cvmliftlem13  35283  cvmlift2lem12  35301  satfv1lem  35349  satffunlem1lem2  35390  satffunlem2lem2  35393  satefvfmla1  35412  mrsubcv  35497  mrsubff  35499  mrsubrn  35500  mrsubccat  35505  elmrsubrn  35507  mrsubco  35508  mrsubvrs  35509  mvhf  35545  msubvrs  35547  mclsax  35556  r1peuqusdeg1  35630  linerflx1  36137  linerflx2  36139  fwddifnval  36151  elhf2  36163  neibastop2lem  36348  weiunpo  36453  weiunso  36454  icoreunrn  37347  relowlssretop  37351  sucneqond  37353  matunitlindflem2  37611  poimirlem4  37618  poimirlem20  37634  poimirlem30  37644  broucube  37648  opnmbllem0  37650  areacirclem2  37703  areacirclem4  37705  blssp  37750  sstotbnd2  37768  totbndbnd  37783  prdstotbnd  37788  cnpwstotbnd  37791  heiborlem9  37813  exidcl  37870  exidresid  37873  grpokerinj  37887  iscringd  37992  erimeq2  38670  prter3  38875  toycom  38966  islfld  39055  lshpsmreu  39102  ldualelvbase  39120  ldualssvscl  39151  lkreqN  39163  lkrlspeqN  39164  erng1lem  40981  erngdvlem4  40985  erng0g  40988  erng1r  40989  erngdvlem4-rN  40993  dva0g  41021  dia1dim2  41056  dia1dimid  41057  dia2dimlem5  41062  dvhelvbasei  41082  dvhvaddass  41091  tendoinvcl  41098  tendolinv  41099  tendorinv  41100  dvhgrp  41101  dvhlveclem  41102  cdlemn4  41192  lcfrlem12N  41548  lcfrlem15  41551  lcdvscl  41599  lcdlssvscl  41600  lcdvsass  41601  lcdvs0N  41610  mapdincl  41655  mapdin  41656  mapdlsmcl  41657  mapdcnvatN  41660  mapdpglem2  41667  mapdpglem12  41677  mapdpglem18  41683  mapdpglem21  41686  mapdpglem22  41687  mapdpglem28  41695  mapdpglem30  41696  hdmaprnlem3N  41844  hdmaprnlem3uN  41845  hdmaprnlem7N  41849  hdmaprnlem8N  41850  hdmaprnlem9N  41851  hdmaprnlem3eN  41852  hdmaprnlem16N  41856  hgmapdcl  41884  hgmapval1  41887  hgmaprnlem4N  41893  hdmapinvlem1  41912  fzadd2d  41966  aks6d1c2lem4  42115  sticksstones1  42134  sticksstones8  42141  sticksstones9  42142  sticksstones10  42143  sticksstones11  42144  sticksstones17  42151  sticksstones18  42152  aks6d1c6lem4  42161  rhmqusspan  42173  aks5lem2  42175  mhmcopsr  42537  evlsbagval  42554  evlsevl  42559  evlvvval  42561  evlvvvallem  42562  selvcllem2  42566  evlselv  42575  mhpind  42582  fltnltalem  42650  wepwsolem  43031  kercvrlsm  43072  dfacbasgrp  43097  onexomgt  43230  onexoegt  43233  onov0suclim  43263  cantnftermord  43309  cantnf2  43314  omcl2  43322  ofoaf  43344  ofoafo  43345  grurankcld  44222  grumnudlem  44274  grumnud  44275  inaex  44286  gruex  44287  dvconstbi  44323  cncmpmax  45026  iooabslt  45497  fmul01lt1lem2  45583  limciccioolb  45619  limcicciooub  45635  limsuppnfdlem  45699  climrescn  45746  climxrrelem  45747  climxrre  45748  liminflimsupxrre  45815  xlimmnfvlem2  45831  xlimpnfvlem2  45835  fsumcncf  45876  ioccncflimc  45883  icocncflimc  45887  cncfiooicclem1  45891  dvbdfbdioolem2  45927  dvnmul  45941  dvnprodlem1  45944  stoweidlem26  46024  stoweidlem34  46032  stoweidlem48  46046  stoweidlem59  46057  dirkercncflem3  46103  fourierdlem32  46137  fourierdlem41  46146  fourierdlem51  46155  fourierdlem63  46167  fourierdlem82  46186  fourierdlem85  46189  fourierdlem93  46197  fourierdlem111  46215  fourierdlem114  46218  etransclem35  46267  hspdifhsp  46614  opnvonmbllem1  46630  ovnovollem1  46654  mbfresmf  46737  smfaddlem1  46761  smfsuplem1  46809  smflimsuplem5  46822  setsidel  47377  setsnidel  47378  imasetpreimafvbijlemf  47402  prelspr  47487  upgrimpths  47909  gpgprismgr4cycllem9  48093  rngccatidALTV  48260  rhmsubcALTVlem3  48271  funcringcsetcALTV2lem3  48280  funcringcsetcALTV2lem8  48285  ringccatidALTV  48294  funcringcsetclem3ALTV  48303  funcringcsetclem8ALTV  48308  srhmsubcALTVlem1  48311  srhmsubcALTV  48313  lcosslsp  48427  nnolog2flm1  48579  ffvbr  48844  glbprlem  48953  topdlat  48992  catprs  49000  iinfsubc  49047  iinfconstbaslem  49054  imaid  49143  fthcomf  49146  uptr2  49210  natoppf2  49219  natoppfb  49220  swapf2  49263  swapfiso  49274  swapciso  49275  oppc1stflem  49276  cofuswapf2  49284  fuco22natlem  49334  fucoppcffth  49400  oppcthinco  49428  oppcthinendcALT  49430  thinccisod  49443  termco  49470  termchommo  49474  termcid  49475  termcterm  49502  termcterm2  49503  diagciso  49528  diagcic  49529  funcsn  49530  uobeqterm  49535  mndtccatid  49576  grptcmon  49582  grptcepi  49583  2arwcat  49589  lanval2  49616  ranval2  49619  lanup  49630  ranup  49631  lmddu  49656