Theorem eleqtrrd 2839

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 2742	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrd 2838	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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811

This theorem is referenced by:  3eltr4d  2851  rspc2vd  3885  disjxiun  5082  eldmressnsn  5989  fnsnbg  7119  elimdelov  7463  elovmpt3rab1  7627  fnwelem  8081  tfrlem13  8329  tz7.44-2  8346  omordi  8501  oneo  8516  omeulem2  8518  oeordi  8523  oeeui  8538  nnneo  8591  naddelim  8622  erref  8664  en1uniel  8976  omxpenlem  9016  unblem3  9204  dffi3  9344  ordtypelem10  9442  oismo  9455  cantnff  9595  cantnfp1lem3  9601  cantnflem1  9610  cnfcom  9621  r1ordg  9702  r1pwss  9708  rankwflemb  9717  r1elwf  9720  rankidb  9724  rankonidlem  9752  fseqenlem2  9947  dfac12lem1  10066  dfac12lem2  10067  pwsdompw  10125  ackbij2lem3  10162  ackbij2  10164  cfsmolem  10192  hsmexlem4  10351  ttukeylem3  10433  ttukeylem7  10437  iundom2g  10462  fpwwe2lem8  10561  canthwelem  10573  pwfseqlem4  10585  winalim2  10619  r1wunlim  10660  tskmid  10763  fzopth  13515  predfz  13607  fzoss2  13642  fz1fzo0m1  13665  fzo0addel  13673  fzo0addelr  13674  elfzoext  13677  fzosubel3  13681  elfzomin  13692  elfzonlteqm1  13696  fzoend  13712  fzoopth  13717  fzofzp1  13719  fzofzp1b  13720  peano2fzor  13730  zmodfzo  13853  seqf1olem2  14004  bcn2  14281  swrdccat2  14632  pfxccat1  14664  swrdswrd  14667  pfxccatin12  14695  splfv1  14717  revcl  14723  revlen  14724  revccat  14728  revrev  14729  repswpfx  14747  cshwidxmod  14765  revco  14796  limsupgre  15443  summolem2a  15677  fsumm1  15713  fsumcom2  15736  prodmolem2a  15899  fprodm1  15932  fprodcom2  15949  prmreclem4  16890  prmreclem5  16891  vdwapid1  16946  vdwlem5  16956  vdwlem8  16959  vdwnnlem2  16967  ramub1lem1  16997  ramub1lem2  16998  mrieqvlemd  17595  mreexd  17608  mreexexlemd  17610  catcocl  17651  catass  17652  moni  17703  epii  17710  inviso1  17733  episect  17752  invisoinvl  17757  catsubcat  17806  subccocl  17812  fullsubc  17817  funcco  17838  resf2nd  17862  funcres  17863  fthepi  17897  nati  17925  arwhoma  18012  catccatid  18073  resscatc  18076  catcisolem  18077  catcoppccl  18084  catcfuccl  18085  estrreslem2  18104  funcestrcsetclem3  18108  funcestrcsetclem8  18113  equivestrcsetc  18118  funcsetcestrclem3  18122  funcsetcestrclem8  18128  xpcco  18149  xpcco2  18153  xpccatid  18154  prfcl  18169  catcxpccl  18173  curf12  18193  curf1cl  18194  curf2  18195  curf2cl  18197  curfcl  18198  uncf2  18203  uncfcurf  18205  diag12  18210  diag2  18211  curf2ndf  18213  hofcl  18225  oppchofcl  18226  oyoncl  18236  yonedalem3a  18240  yonedalem4b  18242  yonedalem22  18244  yonedalem3b  18245  yonedalem3  18246  yonedainv  18247  yonffthlem  18248  latcl2  18402  latlem  18403  latjcom  18413  latmcom  18429  clatlem  18468  clatlubcl2  18470  clatglbcl2  18472  acsfiindd  18519  pfxchn  18576  chnind  18587  chnub  18588  chnlt  18589  chnccat  18592  chnrev  18593  gsumpropd2lem  18647  sgrppropd  18699  mndpropd  18727  imasmnd  18743  frmdmnd  18827  frmdgsum  18830  grpsubpropd2  19022  imasgrp  19032  subg0  19108  0ghm  19205  resghm2  19208  ghmco  19211  pwsdiagghm  19219  ghmqusnsglem2  19256  ghmqusnsg  19257  ghmquskerlem2  19260  ghmquskerlem3  19261  ghmqusker  19262  psgnunilem1  19468  psgnunilem5  19469  psgnunilem2  19470  psgnunilem3  19471  sylow1lem4  19576  sylow1lem5  19577  efglem  19691  efgtf  19697  efginvrel2  19702  efginvrel1  19703  efgsdmi  19707  efgs1b  19711  efgsres  19713  efgsfo  19714  efgredleme  19718  efgredlemc  19720  efgredlem  19722  efgcpbllemb  19730  frgp0  19735  frgpadd  19738  frgpinv  19739  vrgpf  19743  vrgpinv  19744  frgpuplem  19747  frgpup1  19750  frgpup2  19751  frgpup3lem  19752  frgpnabllem1  19848  frgpnabllem2  19849  gsumval3  19882  dprdfid  19994  dprdsn  20013  dprd2da  20019  dpjidcl  20035  pgpfac1lem2  20052  pgpfaclem3  20060  ablsimpg1gend  20082  ablsimpgprmd  20092  rngpropd  20155  imasrng  20158  ringpropd  20269  imasring  20310  qusring2  20314  pwsco1rhm  20479  pwsco2rhm  20480  lringuplu  20521  subrgunit  20567  pwsdiagrhm  20584  rnghmsubcsetclem1  20608  zrinitorngc  20619  zrtermorngc  20620  zrzeroorngc  20621  rhmsubcsetclem1  20637  rhmsubcrngclem1  20643  zrtermoringc  20652  zrninitoringc  20653  srhmsubclem2  20655  srhmsubc  20657  cntzsdrg  20779  isabvd  20789  lmodprop2d  20919  islssd  20930  prdsvscacl  20963  prdslmodd  20964  islmhm2  21033  lmhmco  21038  lmhmplusg  21039  lmhmvsca  21040  lmhmpropd  21068  lsppreli  21085  ellspsn4  21122  lssacsex  21142  lspsnat  21143  lidlnsg  21246  qus2idrng  21271  qus1  21272  qusrhm  21274  rhmpreimaidl  21275  rhmqusnsg  21283  rngqiprngghmlem1  21285  rngqiprngfulem1  21309  irinitoringc  21459  nzerooringczr  21460  znf1o  21531  cssmre  21673  dsmmlss  21724  frlmsplit2  21753  frlmbas3  21756  frlmup1  21778  assapropd  21851  psr0cl  21931  psrnegcl  21933  psr1cl  21939  resspsrmul  21954  subrgpsr  21956  mvrf  21963  mplmon  22013  mplcoe1  22015  subrgasclcl  22045  mplind  22048  evlslem1  22060  subrgply1  22196  psrplusgpropd  22199  ply1coe  22263  cply1coe0bi  22267  lply1binomsc  22276  ply1fermltlchr  22277  evls1val  22285  evls1rhm  22287  evl1val  22294  evl1rhm  22297  pf1ind  22320  evl1scvarpw  22328  evls1fpws  22334  mhmcompl  22345  rhmply1  22351  matbas2i  22387  matplusg2  22392  matvsca2  22393  matsubgcell  22399  matvscacell  22401  mpomatmul  22411  mavmulval  22510  mavmulcl  22512  mavmulass  22514  mavmul0  22517  mavmumamul1  22520  m1detdiag  22562  cramerimplem2  22649  mat2pmatmul  22696  mat2pmatlin  22700  monmatcollpw  22744  pmatcollpwfi  22747  mply1topmatcl  22770  pm2mpghm  22781  pm2mpmhmlem2  22784  pm2mp  22790  chpmat1dlem  22800  chpmat1d  22801  chpdmatlem0  22802  chpscmat  22807  chpscmatgsumbin  22809  chpscmatgsummon  22810  chfacfscmulcl  22822  cpmadugsumlemB  22839  cpmadugsumlemC  22840  chcoeffeqlem  22850  cldmreon  23059  neiptopreu  23098  maxlp  23112  ordttopon  23158  ordtrest2lem  23168  cnprcl2  23216  lmcnp  23269  resthauslem  23328  hauscmplem  23371  1stcfb  23410  2ndcctbss  23420  2ndcomap  23423  dis2ndc  23425  loclly  23452  hausllycmp  23459  locfincmp  23491  dissnref  23493  kgeni  23502  kgenidm  23512  ptpjpre2  23545  xkoopn  23554  txopn  23567  ptpjopn  23577  ptcldmpt  23579  ptcls  23581  pthaus  23603  txkgen  23617  xkohaus  23618  xkopt  23620  txconn  23654  imastps  23686  kqid  23693  kqopn  23699  kqcld  23700  isr0  23702  indishmph  23763  pt1hmeo  23771  ptuncnv  23772  ptunhmeo  23773  t0kq  23783  filconn  23848  uzrest  23862  uffixsn  23890  fmfnfmlem2  23920  flimss2  23937  flimss1  23938  flimclslem  23949  flfcnp  23969  fclsfnflim  23992  uffclsflim  23996  fcfelbas  24001  alexsublem  24009  alexsub  24010  cnextcn  24032  cnextfres1  24033  cnextfres  24034  tmdgsum  24060  distgp  24064  indistgp  24065  symgtgp  24071  ghmcnp  24080  qustgpopn  24085  qustgplem  24086  qustgphaus  24088  prdstmdd  24089  prdstgpd  24090  tsmsid  24105  tsmssubm  24108  tsmsmhm  24111  tsmsadd  24112  tsmssplit  24117  utop2nei  24215  utop3cls  24216  neipcfilu  24260  cnextucn  24267  ucnextcn  24268  blpnfctr  24401  lpbl  24468  met2ndci  24487  tmsxps  24501  metcnpi  24509  metcnpi2  24510  metcnpi3  24511  metustid  24519  metustsym  24520  metustexhalf  24521  subgngp  24600  ngptgp  24601  sranlm  24649  nlmvscn  24652  nrginvrcn  24657  lssnlm  24666  nghmcn  24710  iccntr  24787  icccmplem2  24789  msdcn  24807  cncfmptc  24879  cncfmptid  24880  cncfmpt2f  24882  icoopnst  24906  iocopnst  24907  nmoleub2lem3  25082  nmoleub3  25086  nmhmcn  25087  ipcn  25213  cfilfcls  25241  caucfil  25250  equivcau  25267  caubl  25275  flimcfil  25281  cmssmscld  25317  rrxdstprj1  25376  minveclem3b  25395  minveclem4  25399  mulcncf  25413  ovolicc2lem3  25486  ovolicc2lem4  25487  opnmbllem  25568  vitalilem2  25576  mbfsup  25631  mbfinf  25632  mbfi1fseqlem4  25685  limccnp  25858  limccnp2  25859  dvreslem  25876  dvres2lem  25877  dvidlem  25882  dvcnp2  25887  dvcn  25888  dvaddbr  25905  dvmulbr  25906  dvcmul  25911  dvcof  25915  dvcnvlem  25943  dvef  25947  rollelem  25956  dvlip2  25962  dvivthlem1  25975  dvivth  25977  lhop2  25982  lhop  25983  dvcnvrelem1  25984  dvcnvrelem2  25985  dvcnvre  25986  ply1rem  26131  fta1blem  26136  plycpn  26255  plyrem  26271  tayl0  26327  dvtaylp  26335  dvntaylp  26336  dvntaylp0  26337  taylthlem1  26338  taylthlem2  26339  ulmdvlem3  26367  psercn  26391  pserdv  26394  abelth  26406  efabl  26514  efopnlem1  26620  loglesqrt  26725  relogbf  26755  efrlim  26933  dchrghm  27219  dchrptlem3  27229  nodenselem5  27652  nosupres  27671  noinfres  27686  ltslpss  27900  precsexlem11  28209  noseq0  28282  noseqp1  28283  noseqrdgfn  28298  noseqrdgsuc  28300  tgbtwntriv2  28555  tgbtwnne  28558  ercgrg  28585  tgidinside  28639  tgbtwnconn1  28643  tglnne  28696  tglnne0  28708  tglnpt2  28709  tglineneq  28712  ncolncol  28714  coltr3  28716  mirln  28744  mirln2  28745  mirconn  28746  krippenlem  28758  footexALT  28786  footexlem1  28787  footexlem2  28788  colperpexlem3  28800  mideulem2  28802  opphllem  28803  oppne3  28811  opphllem1  28815  opphllem2  28816  opphllem4  28818  oppperpex  28821  opphl  28822  hlpasch  28824  hpgerlem  28833  colhp  28838  midbtwn  28847  lmieu  28852  lmiisolem  28864  sacgr  28899  f1otrg  28939  f1otrge  28940  ebtwntg  29051  ecgrtg  29052  eengtrkg  29055  eengtrkge  29056  upgr1eop  29184  usgredg3  29285  uspgr1eop  29316  usgr1eop  29319  vtxdun  29550  vtxdfiun  29551  1loopgruspgr  29569  1loopgrvd2  29572  1hevtxdg1  29575  1egrvtxdg1  29578  1egrvtxdg0  29580  umgr2v2e  29594  wlkres  29737  wlkp1lem4  29743  wlkp1  29748  cyclnumvtx  29868  wwlksm1edg  29949  wwlksnext  29961  wwlksnextproplem3  29979  clwwlkel  30116  1wlkdlem2  30208  trlsegvdeg  30297  eupth2lem3lem1  30298  eupth2lem3lem2  30299  extwwlkfab  30422  numclwlk2lem2f  30447  spansnid  31634  elspansn4  31644  fnpreimac  32743  ccatf1  33009  ccatws1f1olast  33012  swrdrn2  33014  swrdrn3  33015  swrdf1  33016  splfv3  33018  pwrssmgc  33060  suppgsumssiun  33133  wrdpmtrlast  33154  psgnfzto1stlem  33161  cycpmfv1  33174  cycpmfv2  33175  cycpmco2lem2  33188  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2  33194  cyc3co2  33201  cycpmrn  33204  submarchi  33247  subrdom  33346  fracfld  33369  imaslmod  33413  quslmod  33418  quslmhm  33419  nsgqusf1olem2  33474  lmhmqusker  33477  rhmquskerlem  33485  idlinsubrg  33491  drngidl  33493  rhmpreimaprmidl  33511  qsidomlem2  33513  mxidlprm  33530  opprmxidlabs  33547  qsdrngilem  33554  qsdrngi  33555  qsdrnglem2  33556  idlsrg0g  33566  pidufd  33603  dfufd2lem  33609  fply1  33618  evl1fpws  33624  ressply1evls1  33625  ressply1sub  33630  ply1asclunit  33634  r1plmhm  33670  extvfvcl  33680  evlextv  33686  mplvrpmga  33689  psrmon  33693  psrmonprod  33696  mplmonprod  33698  issply  33705  esplympl  33711  esplyind  33719  drgextlsp  33738  matdim  33759  ply1degltdimlem  33766  lindsunlem  33768  qusdimsum  33772  fedgmullem1  33773  fedgmullem2  33774  fedgmul  33775  extdg1id  33810  evls1fldgencl  33814  irngss  33831  irngnzply1  33835  extdgfialglem1  33836  extdgfialglem2  33837  minplymindeg  33852  minplyirredlem  33854  irredminply  33860  algextdeglem2  33862  constrconj  33889  constrfiss  33895  1smat1  33948  submat1n  33949  lmatfval  33958  lmatcl  33960  mdetpmtr1  33967  madjusmdetlem4  33974  qtopt1  33979  qtophaus  33980  locfinref  33985  zarcls1  34013  zarclsiin  34015  zarmxt1  34024  zarcmplem  34025  rhmpreimacn  34029  ordtrest2NEWlem  34066  elzrhunit  34121  qqhcn  34135  qqhucn  34136  esumel  34191  esumsplit  34197  sigagenss2  34294  elsx  34338  sxbrsigalem0  34415  dya2icoseg  34421  eulerpartlemb  34512  eulerpartlemgvv  34520  iwrdsplit  34531  sseqfv2  34538  probfinmeasb  34572  dstrvprob  34616  dstfrvel  34618  ballotlemrv  34664  signstfvn  34713  signstfvp  34715  signstfveq0  34721  signsvtp  34727  signsvtn  34728  reprsuc  34759  reprpmtf1o  34770  lpadleft  34827  bnj1006  35102  bnj1018g  35105  bnj1018  35106  bnj1121  35127  bnj1398  35176  bnj1450  35192  bnj1501  35209  revpfxsfxrev  35298  swrdrevpfx  35299  pfxwlk  35306  revwlk  35307  swrdwlk  35309  subfacp1lem5  35366  ptpconn  35415  indispconn  35416  cvxsconn  35425  cvmseu  35458  cvmliftmolem2  35464  cvmliftlem7  35473  cvmliftlem10  35476  cvmliftlem13  35478  cvmlift2lem12  35496  satfv1lem  35544  satffunlem1lem2  35585  satffunlem2lem2  35588  satefvfmla1  35607  mrsubcv  35692  mrsubff  35694  mrsubrn  35695  mrsubccat  35700  elmrsubrn  35702  mrsubco  35703  mrsubvrs  35704  mvhf  35740  msubvrs  35742  mclsax  35751  r1peuqusdeg1  35825  linerflx1  36331  linerflx2  36333  fwddifnval  36345  elhf2  36357  neibastop2lem  36542  weiunpo  36647  weiunso  36648  icoreunrn  37675  relowlssretop  37679  sucneqond  37681  matunitlindflem2  37938  poimirlem4  37945  poimirlem20  37961  poimirlem30  37971  broucube  37975  opnmbllem0  37977  areacirclem2  38030  areacirclem4  38032  blssp  38077  sstotbnd2  38095  totbndbnd  38110  prdstotbnd  38115  cnpwstotbnd  38118  heiborlem9  38140  exidcl  38197  exidresid  38200  grpokerinj  38214  iscringd  38319  erimeq2  39084  prter3  39328  toycom  39419  islfld  39508  lshpsmreu  39555  ldualelvbase  39573  ldualssvscl  39604  lkreqN  39616  lkrlspeqN  39617  erng1lem  41433  erngdvlem4  41437  erng0g  41440  erng1r  41441  erngdvlem4-rN  41445  dva0g  41473  dia1dim2  41508  dia1dimid  41509  dia2dimlem5  41514  dvhelvbasei  41534  dvhvaddass  41543  tendoinvcl  41550  tendolinv  41551  tendorinv  41552  dvhgrp  41553  dvhlveclem  41554  cdlemn4  41644  lcfrlem12N  42000  lcfrlem15  42003  lcdvscl  42051  lcdlssvscl  42052  lcdvsass  42053  lcdvs0N  42062  mapdincl  42107  mapdin  42108  mapdlsmcl  42109  mapdcnvatN  42112  mapdpglem2  42119  mapdpglem12  42129  mapdpglem18  42135  mapdpglem21  42138  mapdpglem22  42139  mapdpglem28  42147  mapdpglem30  42148  hdmaprnlem3N  42296  hdmaprnlem3uN  42297  hdmaprnlem7N  42301  hdmaprnlem8N  42302  hdmaprnlem9N  42303  hdmaprnlem3eN  42304  hdmaprnlem16N  42308  hgmapdcl  42336  hgmapval1  42339  hgmaprnlem4N  42345  hdmapinvlem1  42364  fzadd2d  42418  aks6d1c2lem4  42566  sticksstones1  42585  sticksstones8  42592  sticksstones9  42593  sticksstones10  42594  sticksstones11  42595  sticksstones17  42602  sticksstones18  42603  aks6d1c6lem4  42612  rhmqusspan  42624  aks5lem2  42626  mhmcopsr  42992  evlsbagval  43002  evlsevl  43007  evlvvval  43008  evlvvvallem  43009  selvcllem2  43011  evlselv  43020  mhpind  43027  fltnltalem  43095  wepwsolem  43470  kercvrlsm  43511  dfacbasgrp  43536  onexomgt  43669  onexoegt  43672  onov0suclim  43702  cantnftermord  43748  cantnf2  43753  omcl2  43761  ofoaf  43783  ofoafo  43784  grurankcld  44660  grumnudlem  44712  grumnud  44713  inaex  44724  gruex  44725  dvconstbi  44761  cncmpmax  45463  iooabslt  45929  fmul01lt1lem2  46015  limciccioolb  46051  limcicciooub  46065  limsuppnfdlem  46129  climrescn  46176  climxrrelem  46177  climxrre  46178  liminflimsupxrre  46245  xlimmnfvlem2  46261  xlimpnfvlem2  46265  fsumcncf  46306  ioccncflimc  46313  icocncflimc  46317  cncfiooicclem1  46321  dvbdfbdioolem2  46357  dvnmul  46371  dvnprodlem1  46374  stoweidlem26  46454  stoweidlem34  46462  stoweidlem48  46476  stoweidlem59  46487  dirkercncflem3  46533  fourierdlem32  46567  fourierdlem41  46576  fourierdlem51  46585  fourierdlem63  46597  fourierdlem82  46616  fourierdlem85  46619  fourierdlem93  46627  fourierdlem111  46645  fourierdlem114  46648  etransclem35  46697  hoicvr  46976  hspdifhsp  47044  opnvonmbllem1  47060  ovnovollem1  47084  mbfresmf  47167  smfaddlem1  47191  smfsuplem1  47239  smflimsuplem5  47252  chnerlem2  47313  setsidel  47836  setsnidel  47837  imasetpreimafvbijlemf  47861  prelspr  47946  upgrimpths  48385  gpgprismgr4cycllem9  48579  rngccatidALTV  48748  rhmsubcALTVlem3  48759  funcringcsetcALTV2lem3  48768  funcringcsetcALTV2lem8  48773  ringccatidALTV  48782  funcringcsetclem3ALTV  48791  funcringcsetclem8ALTV  48796  srhmsubcALTVlem1  48799  srhmsubcALTV  48801  lcosslsp  48914  nnolog2flm1  49066  ffvbr  49331  glbprlem  49440  topdlat  49479  catprs  49486  iinfsubc  49533  iinfconstbaslem  49540  imaid  49629  fthcomf  49632  uptr2  49696  natoppf2  49705  natoppfb  49706  swapf2  49749  swapfiso  49760  swapciso  49761  oppc1stflem  49762  cofuswapf2  49770  fuco22natlem  49820  fucoppcffth  49886  oppcthinco  49914  oppcthinendcALT  49916  thinccisod  49929  termco  49956  termchommo  49960  termcid  49961  termcterm  49988  termcterm2  49989  diagciso  50014  diagcic  50015  funcsn  50016  uobeqterm  50021  mndtccatid  50062  grptcmon  50068  grptcepi  50069  2arwcat  50075  lanval2  50102  ranval2  50105  lanup  50116  ranup  50117  lmddu  50142