Theorem eleqtrrd 2872

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  3eltr4d  2884  rspc2vd  3909  disjxiun  5110  eldmressnsn  6026  fnsnbg  7165  elimdelov  7509  elovmpt3rab1  7673  fnwelem  8129  tfrlem13  8379  tz7.44-2  8396  omordi  8553  oneo  8568  omeulem2  8570  oeordi  8575  oeeui  8590  nnneo  8643  naddelim  8675  erref  8717  en1uniel  9028  omxpenlem  9068  unblem3  9256  dffi3  9393  ordtypelem10  9491  oismo  9504  cantnff  9645  cantnfp1lem3  9651  cantnflem1  9660  cnfcom  9671  r1ordg  9752  r1pwss  9758  rankwflemb  9767  r1elwf  9770  rankidb  9774  rankonidlem  9802  fseqenlem2  10011  dfac12lem1  10129  dfac12lem2  10130  pwsdompw  10188  ackbij2lem3  10225  ackbij2  10227  cfsmolem  10256  hsmexlem4  10415  ttukeylem3  10497  ttukeylem7  10501  iundom2g  10526  fpwwe2lem8  10625  canthwelem  10637  pwfseqlem4  10649  winalim2  10683  r1wunlim  10724  tskmid  10827  fzopth  13591  predfz  13683  fzoss2  13718  fz1fzo0m1  13741  fzo0addel  13749  fzo0addelr  13750  elfzoext  13753  fzosubel3  13757  elfzomin  13768  elfzonlteqm1  13772  fzoend  13788  fzoopth  13793  fzofzp1  13795  fzofzp1b  13796  peano2fzor  13806  zmodfzo  13929  seqf1olem2  14080  bcn2  14357  swrdccat2  14709  pfxccat1  14741  swrdswrd  14744  pfxccatin12  14772  splfv1  14794  revcl  14800  revlen  14801  revccat  14805  revrev  14806  repswpfx  14824  cshwidxmod  14842  revco  14873  limsupgre  15534  summolem2a  15768  fsumm1  15804  fsumcom2  15827  prodmolem2a  15990  fprodm1  16023  fprodcom2  16040  prmreclem4  16981  prmreclem5  16982  vdwapid1  17037  vdwlem5  17047  vdwlem8  17050  vdwnnlem2  17058  ramub1lem1  17088  ramub1lem2  17089  mrieqvlemd  17687  mreexd  17700  mreexexlemd  17702  catcocl  17743  catass  17744  moni  17795  epii  17802  inviso1  17825  episect  17844  invisoinvl  17849  catsubcat  17898  subccocl  17904  fullsubc  17909  funcco  17930  resf2nd  17954  funcres  17955  fthepi  17989  nati  18017  arwhoma  18104  catccatid  18165  resscatc  18168  catcisolem  18169  catcoppccl  18176  catcfuccl  18177  estrreslem2  18196  funcestrcsetclem3  18200  funcestrcsetclem8  18205  equivestrcsetc  18210  funcsetcestrclem3  18214  funcsetcestrclem8  18220  xpcco  18241  xpcco2  18245  xpccatid  18246  prfcl  18261  catcxpccl  18265  curf12  18285  curf1cl  18286  curf2  18287  curf2cl  18289  curfcl  18290  uncf2  18295  uncfcurf  18297  diag12  18302  diag2  18303  curf2ndf  18305  hofcl  18317  oppchofcl  18318  oyoncl  18328  yonedalem3a  18332  yonedalem4b  18334  yonedalem22  18336  yonedalem3b  18337  yonedalem3  18338  yonedainv  18339  yonffthlem  18340  latcl2  18494  latlem  18495  latjcom  18505  latmcom  18521  clatlem  18560  clatlubcl2  18562  clatglbcl2  18564  acsfiindd  18611  pfxchn  18668  chnind  18679  chnub  18680  chnlt  18681  chnccat  18684  chnrev  18685  gsumpropd2lem  18739  sgrppropd  18791  mndpropd  18819  imasmnd  18835  frmdmnd  18920  frmdgsum  18923  grpsubpropd2  19114  imasgrp  19124  subg0  19200  0ghm  19302  resghm2  19305  ghmco  19308  pwsdiagghm  19316  ghmqusnsglem2  19353  ghmqusnsg  19354  ghmquskerlem2  19357  ghmquskerlem3  19358  ghmqusker  19359  psgnunilem1  19565  psgnunilem5  19566  psgnunilem2  19567  psgnunilem3  19568  sylow1lem4  19673  sylow1lem5  19674  efglem  19788  efgtf  19794  efginvrel2  19799  efginvrel1  19800  efgsdmi  19804  efgs1b  19808  efgsres  19810  efgsfo  19811  efgredleme  19815  efgredlemc  19817  efgredlem  19819  efgcpbllemb  19827  frgp0  19832  frgpadd  19835  frgpinv  19836  vrgpf  19840  vrgpinv  19841  frgpuplem  19844  frgpup1  19847  frgpup2  19848  frgpup3lem  19849  frgpnabllem1  19945  frgpnabllem2  19946  gsumval3  19979  dprdfid  20091  dprdsn  20110  dprd2da  20116  dpjidcl  20132  pgpfac1lem2  20149  pgpfaclem3  20157  ablsimpg1gend  20179  ablsimpgprmd  20189  rngpropd  20254  imasrng  20257  ringpropd  20373  imasring  20414  qusring2  20418  pwsco1rhm  20586  pwsco2rhm  20587  lringuplu  20631  subrgunit  20677  pwsdiagrhm  20694  rnghmsubcsetclem1  20718  zrinitorngc  20729  zrtermorngc  20730  zrzeroorngc  20731  rhmsubcsetclem1  20747  rhmsubcrngclem1  20753  zrtermoringc  20762  zrninitoringc  20763  srhmsubclem2  20765  srhmsubc  20767  cntzsdrg  20885  isabvd  20895  lmodprop2d  21025  islssd  21036  prdsvscacl  21069  prdslmodd  21070  islmhm2  21139  lmhmco  21144  lmhmplusg  21145  lmhmvsca  21146  lmhmpropd  21174  lsppreli  21191  ellspsn4  21228  lssacsex  21248  lspsnat  21249  lidlnsg  21358  qus2idrng  21385  qus1  21386  qusrhm  21388  rhmpreimaidl  21389  rhmqusnsg  21398  rngqiprngghmlem1  21400  rngqiprngfulem1  21424  rhmpreimaprmidl  21450  qsidomlem2  21452  irinitoringc  21600  nzerooringczr  21601  znf1o  21672  cssmre  21814  dsmmlss  21865  frlmsplit2  21894  frlmbas3  21897  frlmup1  21919  assapropd  21992  psr0cl  22073  psrnegcl  22075  psr1cl  22081  resspsrmul  22096  subrgpsr  22098  mvrf  22105  mplmon  22157  mplcoe1  22159  subrgasclcl  22189  mplind  22192  evlslem1  22204  mhmcompl  22243  evlsevl  22254  evlvvval  22255  selvcllem2  22257  subrgply1  22363  psrplusgpropd  22366  ply1coe  22429  cply1coe0bi  22433  lply1binomsc  22442  ply1fermltlchr  22443  evls1val  22451  evls1rhm  22453  evl1val  22460  evl1rhm  22463  pf1ind  22486  evl1scvarpw  22494  evls1fpws  22500  rhmply1  22514  matbas2i  22550  matplusg2  22555  matvsca2  22556  matsubgcell  22562  matvscacell  22564  mpomatmul  22574  mavmulval  22673  mavmulcl  22675  mavmulass  22677  mavmul0  22680  mavmumamul1  22683  m1detdiag  22725  cramerimplem2  22812  mat2pmatmul  22859  mat2pmatlin  22863  monmatcollpw  22907  pmatcollpwfi  22910  mply1topmatcl  22933  pm2mpghm  22944  pm2mpmhmlem2  22947  pm2mp  22953  chpmat1dlem  22963  chpmat1d  22964  chpdmatlem0  22965  chpscmat  22970  chpscmatgsumbin  22972  chpscmatgsummon  22973  chfacfscmulcl  22985  cpmadugsumlemB  23002  cpmadugsumlemC  23003  chcoeffeqlem  23013  cldmreon  23222  neiptopreu  23261  maxlp  23275  ordttopon  23321  ordtrest2lem  23331  cnprcl2  23379  lmcnp  23432  resthauslem  23491  hauscmplem  23534  1stcfb  23573  2ndcctbss  23583  2ndcomap  23586  dis2ndc  23588  loclly  23615  hausllycmp  23622  locfincmp  23654  dissnref  23656  kgeni  23665  kgenidm  23675  ptpjpre2  23708  xkoopn  23717  txopn  23730  ptpjopn  23740  ptcldmpt  23742  ptcls  23744  pthaus  23766  txkgen  23780  xkohaus  23781  xkopt  23783  txconn  23817  imastps  23849  kqid  23856  kqopn  23862  kqcld  23863  isr0  23865  indishmph  23926  pt1hmeo  23934  ptuncnv  23935  ptunhmeo  23936  t0kq  23946  filconn  24011  uzrest  24025  uffixsn  24053  fmfnfmlem2  24083  flimss2  24100  flimss1  24101  flimclslem  24112  flfcnp  24132  fclsfnflim  24155  uffclsflim  24159  fcfelbas  24164  alexsublem  24172  alexsub  24173  cnextcn  24195  cnextfres1  24196  cnextfres  24197  tmdgsum  24223  distgp  24227  indistgp  24228  symgtgp  24234  ghmcnp  24243  qustgpopn  24248  qustgplem  24249  qustgphaus  24251  prdstmdd  24252  prdstgpd  24253  tsmsid  24268  tsmssubm  24271  tsmsmhm  24274  tsmsadd  24275  tsmssplit  24280  utop2nei  24378  utop3cls  24379  neipcfilu  24423  cnextucn  24430  ucnextcn  24431  blpnfctr  24564  lpbl  24631  met2ndci  24650  tmsxps  24664  metcnpi  24672  metcnpi2  24673  metcnpi3  24674  metustid  24682  metustsym  24683  metustexhalf  24684  subgngp  24763  ngptgp  24764  sranlm  24812  nlmvscn  24815  nrginvrcn  24820  lssnlm  24829  nghmcn  24873  iccntr  24950  icccmplem2  24952  msdcn  24970  cncfmptc  25042  cncfmptid  25043  cncfmpt2f  25045  icoopnst  25069  iocopnst  25070  nmoleub2lem3  25245  nmoleub3  25249  nmhmcn  25250  ipcn  25376  cfilfcls  25404  caucfil  25413  equivcau  25430  caubl  25438  flimcfil  25444  cmssmscld  25480  rrxdstprj1  25539  minveclem3b  25558  minveclem4  25562  mulcncf  25576  ovolicc2lem3  25649  ovolicc2lem4  25650  opnmbllem  25731  vitalilem2  25739  mbfsup  25794  mbfinf  25795  mbfi1fseqlem4  25848  limccnp  26021  limccnp2  26022  dvreslem  26039  dvres2lem  26040  dvidlem  26045  dvcnp2  26050  dvcn  26051  dvaddbr  26068  dvmulbr  26069  dvcmul  26074  dvcof  26078  dvcnvlem  26106  dvef  26110  rollelem  26119  dvlip2  26125  dvivthlem1  26138  dvivth  26140  lhop2  26145  lhop  26146  dvcnvrelem1  26147  dvcnvrelem2  26148  dvcnvre  26149  ply1rem  26294  fta1blem  26299  plycpn  26421  plyrem  26437  tayl0  26493  dvtaylp  26501  dvntaylp  26502  dvntaylp0  26503  taylthlem1  26504  taylthlem2  26505  ulmdvlem3  26533  psercn  26557  pserdv  26560  abelth  26572  efabl  26683  efopnlem1  26789  loglesqrt  26894  relogbf  26924  efrlim  27102  dchrghm  27388  dchrptlem3  27398  nodenselem5  27820  nosupres  27839  noinfres  27854  ltslpss  28069  precsexlem11  28378  noseq0  28451  noseqp1  28452  noseqrdgfn  28467  noseqrdgsuc  28469  tgbtwntriv2  28724  tgbtwnne  28727  ercgrg  28754  tgidinside  28808  tgbtwnconn1  28812  tglnne  28865  tglinesseq  28877  tglnne0  28878  tglineneq  28882  ncolncol  28884  coltr3  28886  tglnpt2  28890  tglnpt3  28891  mirln  28917  mirln2  28918  mirconn  28919  krippenlem  28931  footexALT  28959  footexlem1  28960  footexlem2  28961  colperpexlem3  28974  mideulem2  28976  opphllem  28977  oppne3  28985  opphllem1  28989  opphllem2  28990  opphllem4  28992  oppperpex  28995  opphl  28996  hlpasch  28999  hpgerlem  29008  colhp  29013  plngval  29019  lnincplng  29026  plngrotlem1  29029  lnssplnglem  29033  plng3p  29039  midbtwn  29048  lmieu  29053  lmiisolem  29065  sacgr  29101  perpeqlem  29107  prlnghpg  29153  prlngmolem1  29157  f1otrg  29163  f1otrge  29164  ebtwntg  29275  ecgrtg  29276  eengtrkg  29279  eengtrkge  29280  upgr1eop  29408  usgredg3  29509  uspgr1eop  29540  usgr1eop  29543  vtxdun  29774  vtxdfiun  29775  1loopgruspgr  29793  1loopgrvd2  29796  1hevtxdg1  29799  1egrvtxdg1  29802  1egrvtxdg0  29804  umgr2v2e  29818  wlkres  29961  wlkp1lem4  29967  wlkp1  29972  cyclnumvtx  30092  wwlksm1edg  30173  wwlksnext  30185  wwlksnextproplem3  30203  clwwlkel  30340  1wlkdlem2  30432  trlsegvdeg  30521  eupth2lem3lem1  30522  eupth2lem3lem2  30523  extwwlkfab  30646  numclwlk2lem2f  30671  spansnid  31858  elspansn4  31868  fnpreimac  32958  ccatf1  33212  ccatws1f1olast  33215  swrdrn2  33217  swrdrn3  33218  swrdf1  33219  splfv3  33221  pwrssmgc  33263  suppgsumssiun  33335  wrdpmtrlast  33356  psgnfzto1stlem  33363  cycpmfv1  33376  cycpmfv2  33377  cycpmco2lem2  33390  cycpmco2lem4  33392  cycpmco2lem5  33393  cycpmco2lem6  33394  cycpmco2  33396  cyc3co2  33403  cycpmrn  33406  submarchi  33449  subrdom  33548  fracfld  33574  imaslmod  33618  quslmod  33623  quslmhm  33624  nsgqusf1olem2  33669  lmhmqusker  33672  rhmquskerlem  33679  idlinsubrg  33685  drngidl  33687  mxidlprm  33700  opprmxidlabs  33716  qsdrngilem  33723  qsdrngi  33724  qsdrnglem2  33725  idlsrg0g  33743  pidufd  33780  dfufd2lem  33786  fply1  33795  evl1fpws  33801  ressply1evls1  33802  ressply1sub  33807  ply1asclunit  33811  r1plmhm  33846  0mplrim  33851  selvascl  33854  selvply1rhmlema  33855  selvply1rhmlem1  33857  extvfvcl  33873  evlextv  33879  mplvrpmga  33882  psrmon  33886  psrmonprod  33889  mplmonprod  33891  issply  33898  esplympl  33904  esplyind  33912  drgextlsp  33931  matdim  33952  ply1degltdimlem  33959  lindsunlem  33961  qusdimsum  33965  fedgmullem1  33966  fedgmullem2  33967  fedgmul  33968  extdg1id  34003  evls1fldgencl  34007  irngss  34024  irngnzply1  34028  extdgfialglem1  34029  extdgfialglem2  34030  minplymindeg  34045  minplyirredlem  34047  irredminply  34053  algextdeglem2  34055  constrconj  34082  constrfiss  34088  1smat1  34141  submat1n  34142  lmatfval  34151  lmatcl  34153  mdetpmtr1  34160  madjusmdetlem4  34167  qtopt1  34172  qtophaus  34173  locfinref  34178  zarcls1  34206  zarclsiin  34208  zarmxt1  34217  zarcmplem  34218  rhmpreimacn  34222  ordtrest2NEWlem  34259  elzrhunit  34314  qqhcn  34328  qqhucn  34329  esumel  34384  esumsplit  34390  sigagenss2  34487  elsx  34531  sxbrsigalem0  34608  dya2icoseg  34614  eulerpartlemb  34705  eulerpartlemgvv  34713  iwrdsplit  34724  sseqfv2  34731  probfinmeasb  34765  dstrvprob  34809  dstfrvel  34811  ballotlemrv  34857  signstfvn  34903  signstfvp  34905  signstfveq0  34911  signsvtp  34917  signsvtn  34918  reprsuc  34949  reprpmtf1o  34960  morleylemrneab  35005  lpadleft  35020  bnj1006  35295  bnj1018g  35298  bnj1018  35299  bnj1121  35320  bnj1398  35369  bnj1450  35385  bnj1501  35402  revpfxsfxrev  35542  swrdrevpfx  35543  pfxwlk  35551  revwlk  35552  swrdwlk  35554  subfacp1lem5  35611  ptpconn  35660  indispconn  35661  cvxsconn  35670  cvmseu  35703  cvmliftmolem2  35709  cvmliftlem7  35718  cvmliftlem10  35721  cvmliftlem13  35723  cvmlift2lem12  35741  satfv1lem  35789  satffunlem1lem2  35830  satffunlem2lem2  35833  satefvfmla1  35852  mrsubcv  35937  mrsubff  35939  mrsubrn  35940  mrsubccat  35945  elmrsubrn  35947  mrsubco  35948  mrsubvrs  35949  mvhf  35985  msubvrs  35987  mclsax  35996  r1peuqusdeg1  36070  linerflx1  36576  linerflx2  36578  fwddifnval  36590  elhf2  36602  neibastop2lem  36796  weiunpo  36901  weiunso  36902  icoreunrn  37930  relowlssretop  37934  sucneqond  37936  matunitlindflem2  38193  poimirlem4  38200  poimirlem20  38216  poimirlem30  38226  broucube  38230  opnmbllem0  38232  areacirclem2  38285  areacirclem4  38287  blssp  38332  sstotbnd2  38350  totbndbnd  38365  prdstotbnd  38370  cnpwstotbnd  38373  heiborlem9  38395  exidcl  38452  exidresid  38455  grpokerinj  38469  iscringd  38574  erimeq2  39339  prter3  39583  toycom  39674  islfld  39763  lshpsmreu  39810  ldualelvbase  39828  ldualssvscl  39859  lkreqN  39871  lkrlspeqN  39872  erng1lem  41688  erngdvlem4  41692  erng0g  41695  erng1r  41696  erngdvlem4-rN  41700  dva0g  41728  dia1dim2  41763  dia1dimid  41764  dia2dimlem5  41769  dvhelvbasei  41789  dvhvaddass  41798  tendoinvcl  41805  tendolinv  41806  tendorinv  41807  dvhgrp  41808  dvhlveclem  41809  cdlemn4  41899  lcfrlem12N  42255  lcfrlem15  42258  lcdvscl  42306  lcdlssvscl  42307  lcdvsass  42308  lcdvs0N  42317  mapdincl  42362  mapdin  42363  mapdlsmcl  42364  mapdcnvatN  42367  mapdpglem2  42374  mapdpglem12  42384  mapdpglem18  42390  mapdpglem21  42393  mapdpglem22  42394  mapdpglem28  42402  mapdpglem30  42403  hdmaprnlem3N  42551  hdmaprnlem3uN  42552  hdmaprnlem7N  42556  hdmaprnlem8N  42557  hdmaprnlem9N  42558  hdmaprnlem3eN  42559  hdmaprnlem16N  42563  hgmapdcl  42591  hgmapval1  42594  hgmaprnlem4N  42600  hdmapinvlem1  42619  fzadd2d  42673  aks6d1c2lem4  42821  sticksstones1  42840  sticksstones8  42847  sticksstones9  42848  sticksstones10  42849  sticksstones11  42850  sticksstones17  42857  sticksstones18  42858  aks6d1c6lem4  42867  rhmqusspan  42879  aks5lem2  42881  mhmcopsr  43241  evlsbagval  43247  evlvvvallem  43248  evlselv  43250  mhpind  43255  fltnltalem  43323  wepwsolem  43698  kercvrlsm  43739  dfacbasgrp  43764  onexomgt  43897  onexoegt  43900  onov0suclim  43930  cantnftermord  43976  cantnf2  43981  omcl2  43989  ofoaf  44011  ofoafo  44012  grurankcld  44886  grumnudlem  44924  grumnud  44925  inaex  44936  gruex  44937  dvconstbi  44973  cncmpmax  45681  iooabslt  46144  fmul01lt1lem2  46230  limciccioolb  46266  limcicciooub  46280  limsuppnfdlem  46344  climrescn  46391  climxrrelem  46392  climxrre  46393  liminflimsupxrre  46460  xlimmnfvlem2  46476  xlimpnfvlem2  46480  fsumcncf  46521  ioccncflimc  46528  cncfuni  46529  icocncflimc  46532  cncfiooicclem1  46536  dvbdfbdioolem2  46572  dvnmul  46586  dvnprodlem1  46589  stoweidlem26  46669  stoweidlem34  46677  stoweidlem48  46691  stoweidlem59  46702  dirkercncflem3  46748  fourierdlem32  46782  fourierdlem41  46791  fourierdlem51  46800  fourierdlem63  46812  fourierdlem82  46831  fourierdlem85  46834  fourierdlem93  46842  fourierdlem111  46860  fourierdlem114  46863  etransclem35  46912  hoicvr  47191  hspdifhsp  47259  opnvonmbllem1  47275  ovnovollem1  47299  mbfresmf  47382  smfaddlem1  47406  smfsuplem1  47454  smflimsuplem5  47467  chnerlem2  47528  setsidel  48051  setsnidel  48052  imasetpreimafvbijlemf  48076  prelspr  48161  upgrimpths  48600  gpgprismgr4cycllem9  48794  rngccatidALTV  48963  rhmsubcALTVlem3  48974  funcringcsetcALTV2lem3  48983  funcringcsetcALTV2lem8  48988  ringccatidALTV  48997  funcringcsetclem3ALTV  49006  funcringcsetclem8ALTV  49011  srhmsubcALTVlem1  49014  srhmsubcALTV  49016  lcosslsp  49140  nnolog2flm1  49292  ffvbr  49556  glbprlem  49665  topdlat  49704  catprs  49711  iinfsubc  49758  iinfconstbaslem  49765  imaid  49854  fthcomf  49857  uptr2  49921  natoppf2  49930  natoppfb  49931  swapf2  49974  swapfiso  49985  swapciso  49986  oppc1stflem  49987  cofuswapf2  49995  fuco22natlem  50045  fucoppcffth  50111  oppcthinco  50139  oppcthinendcALT  50141  thinccisod  50154  termco  50181  termchommo  50185  termcid  50186  termcterm  50213  termcterm2  50214  diagciso  50239  diagcic  50240  funcsn  50241  uobeqterm  50246  mndtccatid  50287  grptcmon  50293  grptcepi  50294  2arwcat  50300  lanval2  50327  ranval2  50330  lanup  50341  ranup  50342  lmddu  50367