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  3886  disjxiun  5083  eldmressnsn  5985  fnsnbg  7114  elimdelov  7458  elovmpt3rab1  7622  fnwelem  8076  tfrlem13  8324  tz7.44-2  8341  omordi  8496  oneo  8511  omeulem2  8513  oeordi  8518  oeeui  8533  nnneo  8586  naddelim  8617  erref  8659  en1uniel  8971  omxpenlem  9011  unblem3  9199  dffi3  9339  ordtypelem10  9437  oismo  9450  cantnff  9590  cantnfp1lem3  9596  cantnflem1  9605  cnfcom  9616  r1ordg  9697  r1pwss  9703  rankwflemb  9712  r1elwf  9715  rankidb  9719  rankonidlem  9747  fseqenlem2  9942  dfac12lem1  10061  dfac12lem2  10062  pwsdompw  10120  ackbij2lem3  10157  ackbij2  10159  cfsmolem  10187  hsmexlem4  10346  ttukeylem3  10428  ttukeylem7  10432  iundom2g  10457  fpwwe2lem8  10556  canthwelem  10568  pwfseqlem4  10580  winalim2  10614  r1wunlim  10655  tskmid  10758  fzopth  13510  predfz  13602  fzoss2  13637  fz1fzo0m1  13660  fzo0addel  13668  fzo0addelr  13669  elfzoext  13672  fzosubel3  13676  elfzomin  13687  elfzonlteqm1  13691  fzoend  13707  fzoopth  13712  fzofzp1  13714  fzofzp1b  13715  peano2fzor  13725  zmodfzo  13848  seqf1olem2  13999  bcn2  14276  swrdccat2  14627  pfxccat1  14659  swrdswrd  14662  pfxccatin12  14690  splfv1  14712  revcl  14718  revlen  14719  revccat  14723  revrev  14724  repswpfx  14742  cshwidxmod  14760  revco  14791  limsupgre  15438  summolem2a  15672  fsumm1  15708  fsumcom2  15731  prodmolem2a  15894  fprodm1  15927  fprodcom2  15944  prmreclem4  16885  prmreclem5  16886  vdwapid1  16941  vdwlem5  16951  vdwlem8  16954  vdwnnlem2  16962  ramub1lem1  16992  ramub1lem2  16993  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  18397  latlem  18398  latjcom  18408  latmcom  18424  clatlem  18463  clatlubcl2  18465  clatglbcl2  18467  acsfiindd  18514  pfxchn  18571  chnind  18582  chnub  18583  chnlt  18584  chnccat  18587  chnrev  18588  gsumpropd2lem  18642  sgrppropd  18694  mndpropd  18722  imasmnd  18738  frmdmnd  18822  frmdgsum  18825  grpsubpropd2  19017  imasgrp  19027  subg0  19103  0ghm  19200  resghm2  19203  ghmco  19206  pwsdiagghm  19214  ghmqusnsglem2  19251  ghmqusnsg  19252  ghmquskerlem2  19255  ghmquskerlem3  19256  ghmqusker  19257  psgnunilem1  19463  psgnunilem5  19464  psgnunilem2  19465  psgnunilem3  19466  sylow1lem4  19571  sylow1lem5  19572  efglem  19686  efgtf  19692  efginvrel2  19697  efginvrel1  19698  efgsdmi  19702  efgs1b  19706  efgsres  19708  efgsfo  19709  efgredleme  19713  efgredlemc  19715  efgredlem  19717  efgcpbllemb  19725  frgp0  19730  frgpadd  19733  frgpinv  19734  vrgpf  19738  vrgpinv  19739  frgpuplem  19742  frgpup1  19745  frgpup2  19746  frgpup3lem  19747  frgpnabllem1  19843  frgpnabllem2  19844  gsumval3  19877  dprdfid  19989  dprdsn  20008  dprd2da  20014  dpjidcl  20030  pgpfac1lem2  20047  pgpfaclem3  20055  ablsimpg1gend  20077  ablsimpgprmd  20087  rngpropd  20150  imasrng  20153  ringpropd  20264  imasring  20305  qusring2  20309  pwsco1rhm  20474  pwsco2rhm  20475  lringuplu  20516  subrgunit  20562  pwsdiagrhm  20579  rnghmsubcsetclem1  20603  zrinitorngc  20614  zrtermorngc  20615  zrzeroorngc  20616  rhmsubcsetclem1  20632  rhmsubcrngclem1  20638  zrtermoringc  20647  zrninitoringc  20648  srhmsubclem2  20650  srhmsubc  20652  cntzsdrg  20774  isabvd  20784  lmodprop2d  20914  islssd  20925  prdsvscacl  20958  prdslmodd  20959  islmhm2  21029  lmhmco  21034  lmhmplusg  21035  lmhmvsca  21036  lmhmpropd  21064  lsppreli  21081  ellspsn4  21118  lssacsex  21138  lspsnat  21139  lidlnsg  21242  qus2idrng  21267  qus1  21268  qusrhm  21270  rhmpreimaidl  21271  rhmqusnsg  21279  rngqiprngghmlem1  21281  rngqiprngfulem1  21305  irinitoringc  21473  nzerooringczr  21474  znf1o  21545  cssmre  21687  dsmmlss  21738  frlmsplit2  21767  frlmbas3  21770  frlmup1  21792  assapropd  21865  psr0cl  21945  psrnegcl  21947  psr1cl  21953  resspsrmul  21968  subrgpsr  21970  mvrf  21977  mplmon  22027  mplcoe1  22029  subrgasclcl  22059  mplind  22062  evlslem1  22074  subrgply1  22210  psrplusgpropd  22213  ply1coe  22277  cply1coe0bi  22281  lply1binomsc  22290  ply1fermltlchr  22291  evls1val  22299  evls1rhm  22301  evl1val  22308  evl1rhm  22311  pf1ind  22334  evl1scvarpw  22342  evls1fpws  22348  mhmcompl  22359  rhmply1  22365  matbas2i  22401  matplusg2  22406  matvsca2  22407  matsubgcell  22413  matvscacell  22415  mpomatmul  22425  mavmulval  22524  mavmulcl  22526  mavmulass  22528  mavmul0  22531  mavmumamul1  22534  m1detdiag  22576  cramerimplem2  22663  mat2pmatmul  22710  mat2pmatlin  22714  monmatcollpw  22758  pmatcollpwfi  22761  mply1topmatcl  22784  pm2mpghm  22795  pm2mpmhmlem2  22798  pm2mp  22804  chpmat1dlem  22814  chpmat1d  22815  chpdmatlem0  22816  chpscmat  22821  chpscmatgsumbin  22823  chpscmatgsummon  22824  chfacfscmulcl  22836  cpmadugsumlemB  22853  cpmadugsumlemC  22854  chcoeffeqlem  22864  cldmreon  23073  neiptopreu  23112  maxlp  23126  ordttopon  23172  ordtrest2lem  23182  cnprcl2  23230  lmcnp  23283  resthauslem  23342  hauscmplem  23385  1stcfb  23424  2ndcctbss  23434  2ndcomap  23437  dis2ndc  23439  loclly  23466  hausllycmp  23473  locfincmp  23505  dissnref  23507  kgeni  23516  kgenidm  23526  ptpjpre2  23559  xkoopn  23568  txopn  23581  ptpjopn  23591  ptcldmpt  23593  ptcls  23595  pthaus  23617  txkgen  23631  xkohaus  23632  xkopt  23634  txconn  23668  imastps  23700  kqid  23707  kqopn  23713  kqcld  23714  isr0  23716  indishmph  23777  pt1hmeo  23785  ptuncnv  23786  ptunhmeo  23787  t0kq  23797  filconn  23862  uzrest  23876  uffixsn  23904  fmfnfmlem2  23934  flimss2  23951  flimss1  23952  flimclslem  23963  flfcnp  23983  fclsfnflim  24006  uffclsflim  24010  fcfelbas  24015  alexsublem  24023  alexsub  24024  cnextcn  24046  cnextfres1  24047  cnextfres  24048  tmdgsum  24074  distgp  24078  indistgp  24079  symgtgp  24085  ghmcnp  24094  qustgpopn  24099  qustgplem  24100  qustgphaus  24102  prdstmdd  24103  prdstgpd  24104  tsmsid  24119  tsmssubm  24122  tsmsmhm  24125  tsmsadd  24126  tsmssplit  24131  utop2nei  24229  utop3cls  24230  neipcfilu  24274  cnextucn  24281  ucnextcn  24282  blpnfctr  24415  lpbl  24482  met2ndci  24501  tmsxps  24515  metcnpi  24523  metcnpi2  24524  metcnpi3  24525  metustid  24533  metustsym  24534  metustexhalf  24535  subgngp  24614  ngptgp  24615  sranlm  24663  nlmvscn  24666  nrginvrcn  24671  lssnlm  24680  nghmcn  24724  iccntr  24801  icccmplem2  24803  msdcn  24821  cncfmptc  24893  cncfmptid  24894  cncfmpt2f  24896  icoopnst  24920  iocopnst  24921  nmoleub2lem3  25096  nmoleub3  25100  nmhmcn  25101  ipcn  25227  cfilfcls  25255  caucfil  25264  equivcau  25281  caubl  25289  flimcfil  25295  cmssmscld  25331  rrxdstprj1  25390  minveclem3b  25409  minveclem4  25413  mulcncf  25427  ovolicc2lem3  25500  ovolicc2lem4  25501  opnmbllem  25582  vitalilem2  25590  mbfsup  25645  mbfinf  25646  mbfi1fseqlem4  25699  limccnp  25872  limccnp2  25873  dvreslem  25890  dvres2lem  25891  dvidlem  25896  dvcnp2  25901  dvcn  25902  dvaddbr  25919  dvmulbr  25920  dvcmul  25925  dvcof  25929  dvcnvlem  25957  dvef  25961  rollelem  25970  dvlip2  25976  dvivthlem1  25989  dvivth  25991  lhop2  25996  lhop  25997  dvcnvrelem1  25998  dvcnvrelem2  25999  dvcnvre  26000  ply1rem  26145  fta1blem  26150  plycpn  26270  plyrem  26286  tayl0  26342  dvtaylp  26351  dvntaylp  26352  dvntaylp0  26353  taylthlem1  26354  taylthlem2  26355  taylthlem2OLD  26356  ulmdvlem3  26384  psercn  26408  pserdv  26411  abelth  26423  efabl  26531  efopnlem1  26637  loglesqrt  26742  relogbf  26772  efrlim  26950  efrlimOLD  26951  dchrghm  27237  dchrptlem3  27247  nodenselem5  27670  nosupres  27689  noinfres  27704  ltslpss  27918  precsexlem11  28227  noseq0  28300  noseqp1  28301  noseqrdgfn  28316  noseqrdgsuc  28318  tgbtwntriv2  28573  tgbtwnne  28576  ercgrg  28603  tgidinside  28657  tgbtwnconn1  28661  tglnne  28714  tglnne0  28726  tglnpt2  28727  tglineneq  28730  ncolncol  28732  coltr3  28734  mirln  28762  mirln2  28763  mirconn  28764  krippenlem  28776  footexALT  28804  footexlem1  28805  footexlem2  28806  colperpexlem3  28818  mideulem2  28820  opphllem  28821  oppne3  28829  opphllem1  28833  opphllem2  28834  opphllem4  28836  oppperpex  28839  opphl  28840  hlpasch  28842  hpgerlem  28851  colhp  28856  midbtwn  28865  lmieu  28870  lmiisolem  28882  sacgr  28917  f1otrg  28957  f1otrge  28958  ebtwntg  29069  ecgrtg  29070  eengtrkg  29073  eengtrkge  29074  upgr1eop  29202  usgredg3  29303  uspgr1eop  29334  usgr1eop  29337  vtxdun  29569  vtxdfiun  29570  1loopgruspgr  29588  1loopgrvd2  29591  1hevtxdg1  29594  1egrvtxdg1  29597  1egrvtxdg0  29599  umgr2v2e  29613  wlkres  29756  wlkp1lem4  29762  wlkp1  29767  cyclnumvtx  29887  wwlksm1edg  29968  wwlksnext  29980  wwlksnextproplem3  29998  clwwlkel  30135  1wlkdlem2  30227  trlsegvdeg  30316  eupth2lem3lem1  30317  eupth2lem3lem2  30318  extwwlkfab  30441  numclwlk2lem2f  30466  spansnid  31653  elspansn4  31663  fnpreimac  32762  ccatf1  33028  ccatws1f1olast  33031  swrdrn2  33033  swrdrn3  33034  swrdf1  33035  splfv3  33037  pwrssmgc  33079  suppgsumssiun  33152  wrdpmtrlast  33173  psgnfzto1stlem  33180  cycpmfv1  33193  cycpmfv2  33194  cycpmco2lem2  33207  cycpmco2lem4  33209  cycpmco2lem5  33210  cycpmco2lem6  33211  cycpmco2  33213  cyc3co2  33220  cycpmrn  33223  submarchi  33266  subrdom  33365  fracfld  33388  imaslmod  33432  quslmod  33437  quslmhm  33438  nsgqusf1olem2  33493  lmhmqusker  33496  rhmquskerlem  33504  idlinsubrg  33510  drngidl  33512  rhmpreimaprmidl  33530  qsidomlem2  33532  mxidlprm  33549  opprmxidlabs  33566  qsdrngilem  33573  qsdrngi  33574  qsdrnglem2  33575  idlsrg0g  33585  pidufd  33622  dfufd2lem  33628  fply1  33637  evl1fpws  33643  ressply1evls1  33644  ressply1sub  33649  ply1asclunit  33653  r1plmhm  33689  extvfvcl  33699  evlextv  33705  mplvrpmga  33708  psrmon  33712  psrmonprod  33715  mplmonprod  33717  issply  33724  esplympl  33730  esplyind  33738  drgextlsp  33757  matdim  33779  ply1degltdimlem  33786  lindsunlem  33788  qusdimsum  33792  fedgmullem1  33793  fedgmullem2  33794  fedgmul  33795  extdg1id  33830  evls1fldgencl  33834  irngss  33851  irngnzply1  33855  extdgfialglem1  33856  extdgfialglem2  33857  minplymindeg  33872  minplyirredlem  33874  irredminply  33880  algextdeglem2  33882  constrconj  33909  constrfiss  33915  1smat1  33968  submat1n  33969  lmatfval  33978  lmatcl  33980  mdetpmtr1  33987  madjusmdetlem4  33994  qtopt1  33999  qtophaus  34000  locfinref  34005  zarcls1  34033  zarclsiin  34035  zarmxt1  34044  zarcmplem  34045  rhmpreimacn  34049  ordtrest2NEWlem  34086  elzrhunit  34141  qqhcn  34155  qqhucn  34156  esumel  34211  esumsplit  34217  sigagenss2  34314  elsx  34358  sxbrsigalem0  34435  dya2icoseg  34441  eulerpartlemb  34532  eulerpartlemgvv  34540  iwrdsplit  34551  sseqfv2  34558  probfinmeasb  34592  dstrvprob  34636  dstfrvel  34638  ballotlemrv  34684  signstfvn  34733  signstfvp  34735  signstfveq0  34741  signsvtp  34747  signsvtn  34748  reprsuc  34779  reprpmtf1o  34790  lpadleft  34847  bnj1006  35122  bnj1018g  35125  bnj1018  35126  bnj1121  35147  bnj1398  35196  bnj1450  35212  bnj1501  35229  revpfxsfxrev  35318  swrdrevpfx  35319  pfxwlk  35326  revwlk  35327  swrdwlk  35329  subfacp1lem5  35386  ptpconn  35435  indispconn  35436  cvxsconn  35445  cvmseu  35478  cvmliftmolem2  35484  cvmliftlem7  35493  cvmliftlem10  35496  cvmliftlem13  35498  cvmlift2lem12  35516  satfv1lem  35564  satffunlem1lem2  35605  satffunlem2lem2  35608  satefvfmla1  35627  mrsubcv  35712  mrsubff  35714  mrsubrn  35715  mrsubccat  35720  elmrsubrn  35722  mrsubco  35723  mrsubvrs  35724  mvhf  35760  msubvrs  35762  mclsax  35771  r1peuqusdeg1  35845  linerflx1  36351  linerflx2  36353  fwddifnval  36365  elhf2  36377  neibastop2lem  36562  weiunpo  36667  weiunso  36668  icoreunrn  37693  relowlssretop  37697  sucneqond  37699  matunitlindflem2  37956  poimirlem4  37963  poimirlem20  37979  poimirlem30  37989  broucube  37993  opnmbllem0  37995  areacirclem2  38048  areacirclem4  38050  blssp  38095  sstotbnd2  38113  totbndbnd  38128  prdstotbnd  38133  cnpwstotbnd  38136  heiborlem9  38158  exidcl  38215  exidresid  38218  grpokerinj  38232  iscringd  38337  erimeq2  39102  prter3  39346  toycom  39437  islfld  39526  lshpsmreu  39573  ldualelvbase  39591  ldualssvscl  39622  lkreqN  39634  lkrlspeqN  39635  erng1lem  41451  erngdvlem4  41455  erng0g  41458  erng1r  41459  erngdvlem4-rN  41463  dva0g  41491  dia1dim2  41526  dia1dimid  41527  dia2dimlem5  41532  dvhelvbasei  41552  dvhvaddass  41561  tendoinvcl  41568  tendolinv  41569  tendorinv  41570  dvhgrp  41571  dvhlveclem  41572  cdlemn4  41662  lcfrlem12N  42018  lcfrlem15  42021  lcdvscl  42069  lcdlssvscl  42070  lcdvsass  42071  lcdvs0N  42080  mapdincl  42125  mapdin  42126  mapdlsmcl  42127  mapdcnvatN  42130  mapdpglem2  42137  mapdpglem12  42147  mapdpglem18  42153  mapdpglem21  42156  mapdpglem22  42157  mapdpglem28  42165  mapdpglem30  42166  hdmaprnlem3N  42314  hdmaprnlem3uN  42315  hdmaprnlem7N  42319  hdmaprnlem8N  42320  hdmaprnlem9N  42321  hdmaprnlem3eN  42322  hdmaprnlem16N  42326  hgmapdcl  42354  hgmapval1  42357  hgmaprnlem4N  42363  hdmapinvlem1  42382  fzadd2d  42436  aks6d1c2lem4  42584  sticksstones1  42603  sticksstones8  42610  sticksstones9  42611  sticksstones10  42612  sticksstones11  42613  sticksstones17  42620  sticksstones18  42621  aks6d1c6lem4  42630  rhmqusspan  42642  aks5lem2  42644  mhmcopsr  43010  evlsbagval  43020  evlsevl  43025  evlvvval  43026  evlvvvallem  43027  selvcllem2  43029  evlselv  43038  mhpind  43045  fltnltalem  43113  wepwsolem  43492  kercvrlsm  43533  dfacbasgrp  43558  onexomgt  43691  onexoegt  43694  onov0suclim  43724  cantnftermord  43770  cantnf2  43775  omcl2  43783  ofoaf  43805  ofoafo  43806  grurankcld  44682  grumnudlem  44734  grumnud  44735  inaex  44746  gruex  44747  dvconstbi  44783  cncmpmax  45485  iooabslt  45951  fmul01lt1lem2  46037  limciccioolb  46073  limcicciooub  46087  limsuppnfdlem  46151  climrescn  46198  climxrrelem  46199  climxrre  46200  liminflimsupxrre  46267  xlimmnfvlem2  46283  xlimpnfvlem2  46287  fsumcncf  46328  ioccncflimc  46335  icocncflimc  46339  cncfiooicclem1  46343  dvbdfbdioolem2  46379  dvnmul  46393  dvnprodlem1  46396  stoweidlem26  46476  stoweidlem34  46484  stoweidlem48  46498  stoweidlem59  46509  dirkercncflem3  46555  fourierdlem32  46589  fourierdlem41  46598  fourierdlem51  46607  fourierdlem63  46619  fourierdlem82  46638  fourierdlem85  46641  fourierdlem93  46649  fourierdlem111  46667  fourierdlem114  46670  etransclem35  46719  hoicvr  46998  hspdifhsp  47066  opnvonmbllem1  47082  ovnovollem1  47106  mbfresmf  47189  smfaddlem1  47213  smfsuplem1  47261  smflimsuplem5  47274  chnerlem2  47333  setsidel  47852  setsnidel  47853  imasetpreimafvbijlemf  47877  prelspr  47962  upgrimpths  48401  gpgprismgr4cycllem9  48595  rngccatidALTV  48764  rhmsubcALTVlem3  48775  funcringcsetcALTV2lem3  48784  funcringcsetcALTV2lem8  48789  ringccatidALTV  48798  funcringcsetclem3ALTV  48807  funcringcsetclem8ALTV  48812  srhmsubcALTVlem1  48815  srhmsubcALTV  48817  lcosslsp  48930  nnolog2flm1  49082  ffvbr  49347  glbprlem  49456  topdlat  49495  catprs  49502  iinfsubc  49549  iinfconstbaslem  49556  imaid  49645  fthcomf  49648  uptr2  49712  natoppf2  49721  natoppfb  49722  swapf2  49765  swapfiso  49776  swapciso  49777  oppc1stflem  49778  cofuswapf2  49786  fuco22natlem  49836  fucoppcffth  49902  oppcthinco  49930  oppcthinendcALT  49932  thinccisod  49945  termco  49972  termchommo  49976  termcid  49977  termcterm  50004  termcterm2  50005  diagciso  50030  diagcic  50031  funcsn  50032  uobeqterm  50037  mndtccatid  50078  grptcmon  50084  grptcepi  50085  2arwcat  50091  lanval2  50118  ranval2  50121  lanup  50132  ranup  50133  lmddu  50158