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  3899  disjxiun  5089  eldmressnsn  5975  fnsnbg  7100  elimdelov  7445  elovmpt3rab1  7609  fnwelem  8064  tfrlem13  8312  tz7.44-2  8329  omordi  8484  oneo  8499  omeulem2  8501  oeordi  8505  oeeui  8520  nnneo  8573  naddelim  8604  erref  8645  en1uniel  8954  omxpenlem  8995  unblem3  9183  dffi3  9321  ordtypelem10  9419  oismo  9432  cantnff  9570  cantnfp1lem3  9576  cantnflem1  9585  cnfcom  9596  r1ordg  9674  r1pwss  9680  rankwflemb  9689  r1elwf  9692  rankidb  9696  rankonidlem  9724  fseqenlem2  9919  dfac12lem1  10038  dfac12lem2  10039  pwsdompw  10097  ackbij2lem3  10134  ackbij2  10136  cfsmolem  10164  hsmexlem4  10323  ttukeylem3  10405  ttukeylem7  10409  iundom2g  10434  fpwwe2lem8  10532  canthwelem  10544  pwfseqlem4  10556  winalim2  10590  r1wunlim  10631  tskmid  10734  fzopth  13464  predfz  13556  fzoss2  13590  fz1fzo0m1  13613  fzo0addel  13621  fzo0addelr  13622  elfzoext  13625  fzosubel3  13629  elfzomin  13640  elfzonlteqm1  13644  fzoend  13660  fzoopth  13665  fzofzp1  13667  fzofzp1b  13668  peano2fzor  13677  zmodfzo  13798  seqf1olem2  13949  bcn2  14226  swrdccat2  14576  pfxccat1  14608  swrdswrd  14611  pfxccatin12  14639  splfv1  14661  revcl  14667  revlen  14668  revccat  14672  revrev  14673  repswpfx  14691  cshwidxmod  14709  revco  14741  limsupgre  15388  summolem2a  15622  fsumm1  15658  fsumcom2  15681  prodmolem2a  15841  fprodm1  15874  fprodcom2  15891  prmreclem4  16831  prmreclem5  16832  vdwapid1  16887  vdwlem5  16897  vdwlem8  16900  vdwnnlem2  16908  ramub1lem1  16938  ramub1lem2  16939  mrieqvlemd  17535  mreexd  17548  mreexexlemd  17550  catcocl  17591  catass  17592  moni  17643  epii  17650  inviso1  17673  episect  17692  invisoinvl  17697  catsubcat  17746  subccocl  17752  fullsubc  17757  funcco  17778  resf2nd  17802  funcres  17803  fthepi  17837  nati  17865  arwhoma  17952  catccatid  18013  resscatc  18016  catcisolem  18017  catcoppccl  18024  catcfuccl  18025  estrreslem2  18044  funcestrcsetclem3  18048  funcestrcsetclem8  18053  equivestrcsetc  18058  funcsetcestrclem3  18062  funcsetcestrclem8  18068  xpcco  18089  xpcco2  18093  xpccatid  18094  prfcl  18109  catcxpccl  18113  curf12  18133  curf1cl  18134  curf2  18135  curf2cl  18137  curfcl  18138  uncf2  18143  uncfcurf  18145  diag12  18150  diag2  18151  curf2ndf  18153  hofcl  18165  oppchofcl  18166  oyoncl  18176  yonedalem3a  18180  yonedalem4b  18182  yonedalem22  18184  yonedalem3b  18185  yonedalem3  18186  yonedainv  18187  yonffthlem  18188  latcl2  18342  latlem  18343  latjcom  18353  latmcom  18369  clatlem  18408  clatlubcl2  18410  clatglbcl2  18412  acsfiindd  18459  gsumpropd2lem  18553  sgrppropd  18605  mndpropd  18633  imasmnd  18649  frmdmnd  18733  frmdgsum  18736  grpsubpropd2  18925  imasgrp  18935  subg0  19011  0ghm  19109  resghm2  19112  ghmco  19115  pwsdiagghm  19123  ghmqusnsglem2  19160  ghmqusnsg  19161  ghmquskerlem2  19164  ghmquskerlem3  19165  ghmqusker  19166  psgnunilem1  19372  psgnunilem5  19373  psgnunilem2  19374  psgnunilem3  19375  sylow1lem4  19480  sylow1lem5  19481  efglem  19595  efgtf  19601  efginvrel2  19606  efginvrel1  19607  efgsdmi  19611  efgs1b  19615  efgsres  19617  efgsfo  19618  efgredleme  19622  efgredlemc  19624  efgredlem  19626  efgcpbllemb  19634  frgp0  19639  frgpadd  19642  frgpinv  19643  vrgpf  19647  vrgpinv  19648  frgpuplem  19651  frgpup1  19654  frgpup2  19655  frgpup3lem  19656  frgpnabllem1  19752  frgpnabllem2  19753  gsumval3  19786  dprdfid  19898  dprdsn  19917  dprd2da  19923  dpjidcl  19939  pgpfac1lem2  19956  pgpfaclem3  19964  ablsimpg1gend  19986  ablsimpgprmd  19996  rngpropd  20059  imasrng  20062  ringpropd  20173  imasring  20215  qusring2  20219  pwsco1rhm  20387  pwsco2rhm  20388  lringuplu  20429  subrgunit  20475  pwsdiagrhm  20492  rnghmsubcsetclem1  20516  zrinitorngc  20527  zrtermorngc  20528  zrzeroorngc  20529  rhmsubcsetclem1  20545  rhmsubcrngclem1  20551  zrtermoringc  20560  zrninitoringc  20561  srhmsubclem2  20563  srhmsubc  20565  cntzsdrg  20687  isabvd  20697  lmodprop2d  20827  islssd  20838  prdsvscacl  20871  prdslmodd  20872  islmhm2  20942  lmhmco  20947  lmhmplusg  20948  lmhmvsca  20949  lmhmpropd  20977  lsppreli  20994  ellspsn4  21031  lssacsex  21051  lspsnat  21052  lidlnsg  21155  qus2idrng  21180  qus1  21181  qusrhm  21183  rhmpreimaidl  21184  rhmqusnsg  21192  rngqiprngghmlem1  21194  rngqiprngfulem1  21218  irinitoringc  21386  nzerooringczr  21387  znf1o  21458  cssmre  21600  dsmmlss  21651  frlmsplit2  21680  frlmbas3  21683  frlmup1  21705  assapropd  21779  psr0cl  21859  psrnegcl  21861  psr1cl  21868  resspsrmul  21883  subrgpsr  21885  mvrf  21892  mplmon  21940  mplcoe1  21942  subrgasclcl  21972  mplind  21975  evlslem1  21987  subrgply1  22115  psrplusgpropd  22118  ply1coe  22183  cply1coe0bi  22187  lply1binomsc  22196  ply1fermltlchr  22197  evls1val  22205  evls1rhm  22207  evl1val  22214  evl1rhm  22217  pf1ind  22240  evl1scvarpw  22248  evls1fpws  22254  mhmcompl  22265  rhmply1  22271  matbas2i  22307  matplusg2  22312  matvsca2  22313  matsubgcell  22319  matvscacell  22321  mpomatmul  22331  mavmulval  22430  mavmulcl  22432  mavmulass  22434  mavmul0  22437  mavmumamul1  22440  m1detdiag  22482  cramerimplem2  22569  mat2pmatmul  22616  mat2pmatlin  22620  monmatcollpw  22664  pmatcollpwfi  22667  mply1topmatcl  22690  pm2mpghm  22701  pm2mpmhmlem2  22704  pm2mp  22710  chpmat1dlem  22720  chpmat1d  22721  chpdmatlem0  22722  chpscmat  22727  chpscmatgsumbin  22729  chpscmatgsummon  22730  chfacfscmulcl  22742  cpmadugsumlemB  22759  cpmadugsumlemC  22760  chcoeffeqlem  22770  cldmreon  22979  neiptopreu  23018  maxlp  23032  ordttopon  23078  ordtrest2lem  23088  cnprcl2  23136  lmcnp  23189  resthauslem  23248  hauscmplem  23291  1stcfb  23330  2ndcctbss  23340  2ndcomap  23343  dis2ndc  23345  loclly  23372  hausllycmp  23379  locfincmp  23411  dissnref  23413  kgeni  23422  kgenidm  23432  ptpjpre2  23465  xkoopn  23474  txopn  23487  ptpjopn  23497  ptcldmpt  23499  ptcls  23501  pthaus  23523  txkgen  23537  xkohaus  23538  xkopt  23540  txconn  23574  imastps  23606  kqid  23613  kqopn  23619  kqcld  23620  isr0  23622  indishmph  23683  pt1hmeo  23691  ptuncnv  23692  ptunhmeo  23693  t0kq  23703  filconn  23768  uzrest  23782  uffixsn  23810  fmfnfmlem2  23840  flimss2  23857  flimss1  23858  flimclslem  23869  flfcnp  23889  fclsfnflim  23912  uffclsflim  23916  fcfelbas  23921  alexsublem  23929  alexsub  23930  cnextcn  23952  cnextfres1  23953  cnextfres  23954  tmdgsum  23980  distgp  23984  indistgp  23985  symgtgp  23991  ghmcnp  24000  qustgpopn  24005  qustgplem  24006  qustgphaus  24008  prdstmdd  24009  prdstgpd  24010  tsmsid  24025  tsmssubm  24028  tsmsmhm  24031  tsmsadd  24032  tsmssplit  24037  utop2nei  24136  utop3cls  24137  neipcfilu  24181  cnextucn  24188  ucnextcn  24189  blpnfctr  24322  lpbl  24389  met2ndci  24408  tmsxps  24422  metcnpi  24430  metcnpi2  24431  metcnpi3  24432  metustid  24440  metustsym  24441  metustexhalf  24442  subgngp  24521  ngptgp  24522  sranlm  24570  nlmvscn  24573  nrginvrcn  24578  lssnlm  24587  nghmcn  24631  iccntr  24708  icccmplem2  24710  msdcn  24728  cncfmptc  24803  cncfmptid  24804  cncfmpt2f  24806  icoopnst  24834  iocopnst  24835  nmoleub2lem3  25013  nmoleub3  25017  nmhmcn  25018  ipcn  25144  cfilfcls  25172  caucfil  25181  equivcau  25198  caubl  25206  flimcfil  25212  cmssmscld  25248  rrxdstprj1  25307  minveclem3b  25326  minveclem4  25330  mulcncf  25344  ovolicc2lem3  25418  ovolicc2lem4  25419  opnmbllem  25500  vitalilem2  25508  mbfsup  25563  mbfinf  25564  mbfi1fseqlem4  25617  limccnp  25790  limccnp2  25791  dvreslem  25808  dvres2lem  25809  dvidlem  25814  dvcnp2  25819  dvcnp2OLD  25820  dvcn  25821  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  dvcmul  25845  dvcof  25850  dvcnvlem  25878  dvef  25882  rollelem  25891  dvlip2  25898  dvivthlem1  25911  dvivth  25913  lhop2  25918  lhop  25919  dvcnvrelem1  25920  dvcnvrelem2  25921  dvcnvre  25922  ply1rem  26069  fta1blem  26074  plycpn  26195  plyrem  26211  tayl0  26267  dvtaylp  26276  dvntaylp  26277  dvntaylp0  26278  taylthlem1  26279  taylthlem2  26280  taylthlem2OLD  26281  ulmdvlem3  26309  psercn  26334  pserdv  26337  abelth  26349  efabl  26457  efopnlem1  26563  loglesqrt  26669  relogbf  26699  efrlim  26877  efrlimOLD  26878  dchrghm  27165  dchrptlem3  27175  nodenselem5  27598  nosupres  27617  noinfres  27632  sltlpss  27822  precsexlem11  28124  noseq0  28189  noseqp1  28190  noseqrdgfn  28205  noseqrdgsuc  28207  tgbtwntriv2  28432  tgbtwnne  28435  ercgrg  28462  tgidinside  28516  tgbtwnconn1  28520  tglnne  28573  tglnne0  28585  tglnpt2  28586  tglineneq  28589  ncolncol  28591  coltr3  28593  mirln  28621  mirln2  28622  mirconn  28623  krippenlem  28635  footexALT  28663  footexlem1  28664  footexlem2  28665  colperpexlem3  28677  mideulem2  28679  opphllem  28680  oppne3  28688  opphllem1  28692  opphllem2  28693  opphllem4  28695  oppperpex  28698  opphl  28699  hlpasch  28701  hpgerlem  28710  colhp  28715  midbtwn  28724  lmieu  28729  lmiisolem  28741  sacgr  28776  f1otrg  28816  f1otrge  28817  ebtwntg  28927  ecgrtg  28928  eengtrkg  28931  eengtrkge  28932  upgr1eop  29060  usgredg3  29161  uspgr1eop  29192  usgr1eop  29195  vtxdun  29427  vtxdfiun  29428  1loopgruspgr  29446  1loopgrvd2  29449  1hevtxdg1  29452  1egrvtxdg1  29455  1egrvtxdg0  29457  umgr2v2e  29471  wlkres  29614  wlkp1lem4  29620  wlkp1  29625  cyclnumvtx  29745  wwlksm1edg  29826  wwlksnext  29838  wwlksnextproplem3  29856  clwwlkel  29990  1wlkdlem2  30082  trlsegvdeg  30171  eupth2lem3lem1  30172  eupth2lem3lem2  30173  extwwlkfab  30296  numclwlk2lem2f  30321  spansnid  31507  elspansn4  31517  fnpreimac  32615  ccatf1  32891  ccatws1f1olast  32895  swrdrn2  32897  swrdrn3  32898  swrdf1  32899  splfv3  32901  pwrssmgc  32943  pfxchn  32952  chnind  32954  chnub  32955  chnlt  32956  wrdpmtrlast  33036  psgnfzto1stlem  33043  cycpmfv1  33056  cycpmfv2  33057  cycpmco2lem2  33070  cycpmco2lem4  33072  cycpmco2lem5  33073  cycpmco2lem6  33074  cycpmco2  33076  cyc3co2  33083  cycpmrn  33086  submarchi  33129  subrdom  33225  fracfld  33248  imaslmod  33291  quslmod  33296  quslmhm  33297  nsgqusf1olem2  33352  lmhmqusker  33355  rhmquskerlem  33363  idlinsubrg  33369  drngidl  33371  rhmpreimaprmidl  33389  qsidomlem2  33391  mxidlprm  33408  opprmxidlabs  33425  qsdrngilem  33432  qsdrngi  33433  qsdrnglem2  33434  idlsrg0g  33444  pidufd  33481  dfufd2lem  33487  fply1  33494  evl1fpws  33500  ressply1evls1  33501  ressply1sub  33506  ply1asclunit  33510  r1plmhm  33543  mplvrpmga  33548  drgextlsp  33566  matdim  33588  ply1degltdimlem  33595  lindsunlem  33597  qusdimsum  33601  fedgmullem1  33602  fedgmullem2  33603  fedgmul  33604  extdg1id  33639  evls1fldgencl  33643  irngss  33660  irngnzply1  33664  extdgfialglem1  33665  extdgfialglem2  33666  minplymindeg  33681  minplyirredlem  33683  irredminply  33689  algextdeglem2  33691  constrconj  33718  constrfiss  33724  1smat1  33777  submat1n  33778  lmatfval  33787  lmatcl  33789  mdetpmtr1  33796  madjusmdetlem4  33803  qtopt1  33808  qtophaus  33809  locfinref  33814  zarcls1  33842  zarclsiin  33844  zarmxt1  33853  zarcmplem  33854  rhmpreimacn  33858  ordtrest2NEWlem  33895  elzrhunit  33950  qqhcn  33964  qqhucn  33965  esumel  34020  esumsplit  34026  sigagenss2  34123  elsx  34167  sxbrsigalem0  34245  dya2icoseg  34251  eulerpartlemb  34342  eulerpartlemgvv  34350  iwrdsplit  34361  sseqfv2  34368  probfinmeasb  34402  dstrvprob  34446  dstfrvel  34448  ballotlemrv  34494  signstfvn  34543  signstfvp  34545  signstfveq0  34551  signsvtp  34557  signsvtn  34558  reprsuc  34589  reprpmtf1o  34600  lpadleft  34657  bnj1006  34933  bnj1018g  34936  bnj1018  34937  bnj1121  34958  bnj1398  35007  bnj1450  35023  bnj1501  35040  revpfxsfxrev  35099  swrdrevpfx  35100  pfxwlk  35107  revwlk  35108  swrdwlk  35110  subfacp1lem5  35167  ptpconn  35216  indispconn  35217  cvxsconn  35226  cvmseu  35259  cvmliftmolem2  35265  cvmliftlem7  35274  cvmliftlem10  35277  cvmliftlem13  35279  cvmlift2lem12  35297  satfv1lem  35345  satffunlem1lem2  35386  satffunlem2lem2  35389  satefvfmla1  35408  mrsubcv  35493  mrsubff  35495  mrsubrn  35496  mrsubccat  35501  elmrsubrn  35503  mrsubco  35504  mrsubvrs  35505  mvhf  35541  msubvrs  35543  mclsax  35552  r1peuqusdeg1  35626  linerflx1  36133  linerflx2  36135  fwddifnval  36147  elhf2  36159  neibastop2lem  36344  weiunpo  36449  weiunso  36450  icoreunrn  37343  relowlssretop  37347  sucneqond  37349  matunitlindflem2  37607  poimirlem4  37614  poimirlem20  37630  poimirlem30  37640  broucube  37644  opnmbllem0  37646  areacirclem2  37699  areacirclem4  37701  blssp  37746  sstotbnd2  37764  totbndbnd  37779  prdstotbnd  37784  cnpwstotbnd  37787  heiborlem9  37809  exidcl  37866  exidresid  37869  grpokerinj  37883  iscringd  37988  erimeq2  38666  prter3  38871  toycom  38962  islfld  39051  lshpsmreu  39098  ldualelvbase  39116  ldualssvscl  39147  lkreqN  39159  lkrlspeqN  39160  erng1lem  40976  erngdvlem4  40980  erng0g  40983  erng1r  40984  erngdvlem4-rN  40988  dva0g  41016  dia1dim2  41051  dia1dimid  41052  dia2dimlem5  41057  dvhelvbasei  41077  dvhvaddass  41086  tendoinvcl  41093  tendolinv  41094  tendorinv  41095  dvhgrp  41096  dvhlveclem  41097  cdlemn4  41187  lcfrlem12N  41543  lcfrlem15  41546  lcdvscl  41594  lcdlssvscl  41595  lcdvsass  41596  lcdvs0N  41605  mapdincl  41650  mapdin  41651  mapdlsmcl  41652  mapdcnvatN  41655  mapdpglem2  41662  mapdpglem12  41672  mapdpglem18  41678  mapdpglem21  41681  mapdpglem22  41682  mapdpglem28  41690  mapdpglem30  41691  hdmaprnlem3N  41839  hdmaprnlem3uN  41840  hdmaprnlem7N  41844  hdmaprnlem8N  41845  hdmaprnlem9N  41846  hdmaprnlem3eN  41847  hdmaprnlem16N  41851  hgmapdcl  41879  hgmapval1  41882  hgmaprnlem4N  41888  hdmapinvlem1  41907  fzadd2d  41961  aks6d1c2lem4  42110  sticksstones1  42129  sticksstones8  42136  sticksstones9  42137  sticksstones10  42138  sticksstones11  42139  sticksstones17  42146  sticksstones18  42147  aks6d1c6lem4  42156  rhmqusspan  42168  aks5lem2  42170  mhmcopsr  42532  evlsbagval  42549  evlsevl  42554  evlvvval  42556  evlvvvallem  42557  selvcllem2  42561  evlselv  42570  mhpind  42577  fltnltalem  42645  wepwsolem  43025  kercvrlsm  43066  dfacbasgrp  43091  onexomgt  43224  onexoegt  43227  onov0suclim  43257  cantnftermord  43303  cantnf2  43308  omcl2  43316  ofoaf  43338  ofoafo  43339  grurankcld  44216  grumnudlem  44268  grumnud  44269  inaex  44280  gruex  44281  dvconstbi  44317  cncmpmax  45020  iooabslt  45490  fmul01lt1lem2  45576  limciccioolb  45612  limcicciooub  45628  limsuppnfdlem  45692  climrescn  45739  climxrrelem  45740  climxrre  45741  liminflimsupxrre  45808  xlimmnfvlem2  45824  xlimpnfvlem2  45828  fsumcncf  45869  ioccncflimc  45876  icocncflimc  45880  cncfiooicclem1  45884  dvbdfbdioolem2  45920  dvnmul  45934  dvnprodlem1  45937  stoweidlem26  46017  stoweidlem34  46025  stoweidlem48  46039  stoweidlem59  46050  dirkercncflem3  46096  fourierdlem32  46130  fourierdlem41  46139  fourierdlem51  46148  fourierdlem63  46160  fourierdlem82  46179  fourierdlem85  46182  fourierdlem93  46190  fourierdlem111  46208  fourierdlem114  46211  etransclem35  46260  hspdifhsp  46607  opnvonmbllem1  46623  ovnovollem1  46647  mbfresmf  46730  smfaddlem1  46754  smfsuplem1  46802  smflimsuplem5  46815  setsidel  47370  setsnidel  47371  imasetpreimafvbijlemf  47395  prelspr  47480  upgrimpths  47903  gpgprismgr4cycllem9  48097  rngccatidALTV  48266  rhmsubcALTVlem3  48277  funcringcsetcALTV2lem3  48286  funcringcsetcALTV2lem8  48291  ringccatidALTV  48300  funcringcsetclem3ALTV  48309  funcringcsetclem8ALTV  48314  srhmsubcALTVlem1  48317  srhmsubcALTV  48319  lcosslsp  48433  nnolog2flm1  48585  ffvbr  48850  glbprlem  48959  topdlat  48998  catprs  49006  iinfsubc  49053  iinfconstbaslem  49060  imaid  49149  fthcomf  49152  uptr2  49216  natoppf2  49225  natoppfb  49226  swapf2  49269  swapfiso  49280  swapciso  49281  oppc1stflem  49282  cofuswapf2  49290  fuco22natlem  49340  fucoppcffth  49406  oppcthinco  49434  oppcthinendcALT  49436  thinccisod  49449  termco  49476  termchommo  49480  termcid  49481  termcterm  49508  termcterm2  49509  diagciso  49534  diagcic  49535  funcsn  49536  uobeqterm  49541  mndtccatid  49582  grptcmon  49588  grptcepi  49589  2arwcat  49595  lanval2  49622  ranval2  49625  lanup  49636  ranup  49637  lmddu  49662