Theorem eleqtrrd 2888

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

Syntax hints:   → wi 4   = wceq 1525   ∈ wcel 2083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-cleq 2790  df-clel 2865

This theorem is referenced by:  3eltr4d  2900  disjxiun  4965  eldmressnsn  5783  elimdelov  7113  elovmpt3rab1  7270  fnwelem  7685  tfrlem13  7885  tz7.44-2  7902  omordi  8049  oneo  8064  omeulem2  8066  oeordi  8070  oeeui  8085  nnneo  8135  erref  8166  en1uniel  8436  omxpenlem  8472  unblem3  8625  dffi3  8748  ordtypelem10  8844  oismo  8857  cantnff  8990  cantnfp1lem3  8996  cantnflem1  9005  cnfcom  9016  r1ordg  9060  r1pwss  9066  rankwflemb  9075  r1elwf  9078  rankidb  9082  rankonidlem  9110  fseqenlem2  9304  dfac12lem1  9422  dfac12lem2  9423  pwsdompw  9479  ackbij2lem3  9516  ackbij2  9518  cfsmolem  9545  hsmexlem4  9704  ttukeylem3  9786  ttukeylem7  9790  iundom2g  9815  fpwwe2lem9  9913  canthwelem  9925  pwfseqlem4  9937  winalim2  9971  r1wunlim  10012  tskmid  10115  fzopth  12798  predfz  12886  fzoss2  12919  fz1fzo0m1  12939  fzo0addel  12945  fzo0addelr  12946  fzosubel3  12952  elfzomin  12963  elfzonlteqm1  12967  fzoend  12982  fzofzp1  12988  fzofzp1b  12989  peano2fzor  12998  zmodfzo  13116  seqf1olem2  13264  bcn2  13533  swrdccat2  13871  pfxccat1  13904  swrdswrd  13907  pfxccatin12  13935  splfv1  13957  revcl  13963  revlen  13964  revccat  13968  revrev  13969  repswpfx  13987  cshwidxmod  14005  revco  14036  limsupgre  14676  summolem2a  14909  fsumm1  14943  fsumcom2  14966  prodmolem2a  15125  fprodm1  15158  fprodcom2  15175  prmreclem4  16088  prmreclem5  16089  vdwapid1  16144  vdwlem5  16154  vdwlem8  16157  vdwnnlem2  16165  ramub1lem1  16195  ramub1lem2  16196  mrieqvlemd  16733  mreexd  16746  mreexexlemd  16748  catcocl  16789  catass  16790  moni  16839  epii  16846  inviso1  16869  episect  16888  invisoinvl  16893  catsubcat  16942  subccocl  16948  fullsubc  16953  funcco  16974  resf2nd  16998  funcres  16999  fthepi  17031  nati  17058  arwhoma  17138  catccatid  17195  resscatc  17198  catcisolem  17199  catcoppccl  17201  catcfuccl  17202  estrreslem2  17221  funcestrcsetclem3  17225  funcestrcsetclem8  17230  equivestrcsetc  17235  funcsetcestrclem3  17239  funcsetcestrclem8  17245  xpcco  17266  xpcco2  17270  xpccatid  17271  prfcl  17286  catcxpccl  17290  curf12  17310  curf1cl  17311  curf2  17312  curf2cl  17314  curfcl  17315  uncf2  17320  uncfcurf  17322  diag12  17327  diag2  17328  curf2ndf  17330  hofcl  17342  oppchofcl  17343  oyoncl  17353  yonedalem3a  17357  yonedalem4b  17359  yonedalem22  17361  yonedalem3b  17362  yonedalem3  17363  yonedainv  17364  yonffthlem  17365  latcl2  17491  latlem  17492  latjcom  17502  latmcom  17518  clatlem  17554  clatlubcl2  17556  clatglbcl2  17558  acsfiindd  17620  gsumpropd2lem  17716  mndpropd  17759  imasmnd  17771  frmdmnd  17839  frmdgsum  17842  grpsubpropd2  17966  imasgrp  17976  subg0  18043  0ghm  18117  resghm2  18120  ghmco  18123  pwsdiagghm  18131  psgnunilem1  18356  psgnunilem5  18357  psgnunilem2  18358  psgnunilem3  18359  sylow1lem4  18460  sylow1lem5  18461  efglem  18573  efgtf  18579  efginvrel2  18584  efginvrel1  18585  efgsdmi  18589  efgs1b  18593  efgsres  18595  efgsfo  18596  efgredleme  18600  efgredlemc  18602  efgredlem  18604  efgcpbllemb  18612  frgp0  18617  frgpadd  18620  frgpinv  18621  vrgpf  18625  vrgpinv  18626  frgpuplem  18629  frgpup1  18632  frgpup2  18633  frgpup3lem  18634  frgpnabllem1  18720  frgpnabllem2  18721  gsumval3  18752  dprdfid  18860  dprdsn  18879  dprd2da  18885  dpjidcl  18901  pgpfac1lem2  18918  pgpfaclem3  18926  ringpropd  19026  imasring  19063  qusring2  19064  pwsco1rhm  19184  pwsco2rhm  19185  subrgunit  19247  pwsdiagrhm  19263  cntzsdrg  19275  isabvd  19285  lmodprop2d  19390  islssd  19401  prdsvscacl  19434  prdslmodd  19435  islmhm2  19504  lmhmco  19509  lmhmplusg  19510  lmhmvsca  19511  lmhmpropd  19539  lsppreli  19556  lspsnel4  19590  lssacsex  19610  lspsnat  19611  qus1  19701  qusrhm  19703  assapropd  19793  rnasclassa  19815  psr0cl  19866  psrnegcl  19868  psr1cl  19874  resspsrmul  19889  subrgpsr  19891  mvrf  19896  mplmon  19935  mplcoe1  19937  subrgasclcl  19970  mplind  19973  evlslem1  19986  subrgply1  20088  psrplusgpropd  20091  ply1coe  20151  cply1coe0bi  20155  lply1binomsc  20162  evls1val  20170  evls1rhm  20172  evl1val  20178  evl1rhm  20181  pf1ind  20204  evl1scvarpw  20212  znf1o  20384  cssmre  20523  dsmmlss  20574  frlmsplit2  20603  frlmbas3  20606  frlmup1  20628  matbas2i  20719  matplusg2  20724  matvsca2  20725  matsubgcell  20731  matvscacell  20733  mpomatmul  20743  mavmulval  20842  mavmulcl  20844  mavmulass  20846  mavmul0  20849  mavmumamul1  20852  m1detdiag  20894  cramerimplem2  20981  mat2pmatmul  21027  mat2pmatlin  21031  monmatcollpw  21075  pmatcollpwfi  21078  mply1topmatcl  21101  pm2mpghm  21112  pm2mpmhmlem2  21115  pm2mp  21121  chpmat1dlem  21131  chpmat1d  21132  chpdmatlem0  21133  chpscmat  21138  chpscmatgsumbin  21140  chpscmatgsummon  21141  chfacfscmulcl  21153  cpmadugsumlemB  21170  cpmadugsumlemC  21171  chcoeffeqlem  21181  cldmreon  21390  neiptopreu  21429  maxlp  21443  ordttopon  21489  ordtrest2lem  21499  cnprcl2  21547  lmcnp  21600  resthauslem  21659  hauscmplem  21702  1stcfb  21741  2ndcctbss  21751  2ndcomap  21754  dis2ndc  21756  loclly  21783  hausllycmp  21790  locfincmp  21822  dissnref  21824  kgeni  21833  kgenidm  21843  ptpjpre2  21876  xkoopn  21885  txopn  21898  ptpjopn  21908  ptcldmpt  21910  ptcls  21912  pthaus  21934  txkgen  21948  xkohaus  21949  xkopt  21951  txconn  21985  imastps  22017  kqid  22024  kqopn  22030  kqcld  22031  isr0  22033  indishmph  22094  pt1hmeo  22102  ptuncnv  22103  ptunhmeo  22104  t0kq  22114  filconn  22179  uzrest  22193  uffixsn  22221  fmfnfmlem2  22251  flimss2  22268  flimss1  22269  flimclslem  22280  flfcnp  22300  fclsfnflim  22323  uffclsflim  22327  fcfelbas  22332  alexsublem  22340  alexsub  22341  cnextcn  22363  cnextfres1  22364  cnextfres  22365  tmdgsum  22391  distgp  22395  indistgp  22396  symgtgp  22397  ghmcnp  22410  qustgpopn  22415  qustgplem  22416  qustgphaus  22418  prdstmdd  22419  prdstgpd  22420  tsmsid  22435  tsmssubm  22438  tsmsmhm  22441  tsmsadd  22442  tsmssplit  22447  utop2nei  22546  utop3cls  22547  neipcfilu  22592  cnextucn  22599  ucnextcn  22600  blpnfctr  22733  lpbl  22800  met2ndci  22819  tmsxps  22833  metcnpi  22841  metcnpi2  22842  metcnpi3  22843  metustid  22851  metustsym  22852  metustexhalf  22853  subgngp  22931  ngptgp  22932  sranlm  22980  nlmvscn  22983  nrginvrcn  22988  lssnlm  22997  nghmcn  23041  iccntr  23116  icccmplem2  23118  msdcn  23136  cncfmptc  23206  cncfmptid  23207  cncfmpt2f  23209  icoopnst  23230  iocopnst  23231  nmoleub2lem3  23406  nmoleub3  23410  nmhmcn  23411  ipcn  23536  cfilfcls  23564  caucfil  23573  equivcau  23590  caubl  23598  flimcfil  23604  cmssmscld  23640  rrxdstprj1  23699  minveclem3b  23718  minveclem4  23722  ovolicc2lem3  23807  ovolicc2lem4  23808  opnmbllem  23889  vitalilem2  23897  mbfsup  23952  mbfinf  23953  mbfi1fseqlem4  24006  limccnp  24176  limccnp2  24177  dvreslem  24194  dvres2lem  24195  dvidlem  24200  dvcnp2  24204  dvcn  24205  dvaddbr  24222  dvmulbr  24223  dvcmul  24228  dvcof  24232  dvcnvlem  24260  dvef  24264  rollelem  24273  dvlip2  24279  dvivthlem1  24292  dvivth  24294  lhop2  24299  lhop  24300  dvcnvrelem1  24301  dvcnvrelem2  24302  dvcnvre  24303  ply1rem  24444  fta1blem  24449  plycpn  24565  plyrem  24581  tayl0  24637  dvtaylp  24645  dvntaylp  24646  dvntaylp0  24647  taylthlem1  24648  taylthlem2  24649  ulmdvlem3  24677  psercn  24701  pserdv  24704  abelth  24716  efabl  24819  efopnlem1  24924  loglesqrt  25024  relogbf  25054  efrlim  25233  dchrghm  25518  dchrptlem3  25528  tgbtwntriv2  25959  tgbtwnne  25962  ercgrg  25989  tgidinside  26043  tgbtwnconn1  26047  tglnne  26100  tglnne0  26112  tglnpt2  26113  tglineneq  26116  ncolncol  26118  coltr3  26120  mirln  26148  mirln2  26149  mirconn  26150  krippenlem  26162  footexALT  26190  footexlem1  26191  footexlem2  26192  colperpexlem3  26204  mideulem2  26206  opphllem  26207  oppne3  26215  opphllem1  26219  opphllem2  26220  opphllem4  26222  oppperpex  26225  opphl  26226  hlpasch  26228  hpgerlem  26237  colhp  26242  midbtwn  26251  lmieu  26256  lmiisolem  26268  sacgr  26303  sacgrOLD  26304  f1otrg  26344  f1otrge  26345  ebtwntg  26455  ecgrtg  26456  eengtrkg  26459  eengtrkge  26460  upgr1eop  26587  usgredg3  26685  uspgr1eop  26716  usgr1eop  26719  vtxdun  26950  vtxdfiun  26951  1loopgruspgr  26969  1loopgrvd2  26972  1hevtxdg1  26975  1egrvtxdg1  26978  1egrvtxdg0  26980  umgr2v2e  26994  wlkres  27138  wlkp1lem4  27144  wlkp1  27149  wwlksm1edg  27345  wwlksnext  27357  wwlksnextproplem3  27376  clwwlkccatlem  27453  clwwlkel  27511  1wlkdlem2  27603  trlsegvdeg  27692  eupth2lem3lem1  27693  eupth2lem3lem2  27694  rspc2vd  27732  extwwlkfab  27819  numclwlk2lem2f  27844  spansnid  29027  elspansn4  29037  fnpreimac  30102  cycpmfv1  30398  cycpmfv2  30399  cyc3co2  30415  cycpmrn  30418  submarchi  30449  imaslmod  30572  quslmod  30573  quslmhm  30574  fply1  30575  drgextlsp  30596  matdim  30613  lindsunlem  30620  qusdimsum  30624  fedgmullem1  30625  fedgmullem2  30626  fedgmul  30627  extdg1id  30653  psgnfzto1stlem  30660  1smat1  30680  submat1n  30681  lmatfval  30690  lmatcl  30692  mdetpmtr1  30699  madjusmdetlem4  30706  qtopt1  30712  qtophaus  30713  locfinref  30718  ordtrest2NEWlem  30778  elzrhunit  30833  qqhcn  30845  qqhucn  30846  esumel  30919  esumsplit  30925  sigagenss2  31022  elsx  31066  sxbrsigalem0  31142  dya2icoseg  31148  eulerpartlemb  31239  eulerpartlemgvv  31247  iwrdsplit  31258  sseqfv2  31265  probfinmeasb  31299  dstrvprob  31342  dstfrvel  31344  ballotlemrv  31390  signstfvn  31452  signstfvp  31454  signstfveq0  31460  signsvtp  31466  signsvtn  31467  reprsuc  31499  reprpmtf1o  31510  lpadleft  31567  bnj1006  31843  bnj1018  31846  bnj1121  31867  bnj1398  31916  bnj1450  31932  bnj1501  31949  revpfxsfxrev  31972  swrdrevpfx  31973  pfxwlk  31980  revwlk  31981  swrdwlk  31983  subfacp1lem5  32041  ptpconn  32090  indispconn  32091  cvxsconn  32100  cvmseu  32133  cvmliftmolem2  32139  cvmliftlem7  32148  cvmliftlem10  32151  cvmliftlem13  32153  cvmlift2lem12  32171  satfv1lem  32219  satffunlem1lem2  32260  satffunlem2lem2  32263  satefvfmla1  32282  mrsubcv  32367  mrsubff  32369  mrsubrn  32370  mrsubccat  32375  elmrsubrn  32377  mrsubco  32378  mrsubvrs  32379  mvhf  32415  msubvrs  32417  mclsax  32426  nodenselem5  32803  nosupres  32818  linerflx1  33221  linerflx2  33223  fwddifnval  33235  elhf2  33247  neibastop2lem  33319  icoreunrn  34192  relowlssretop  34196  sucneqond  34198  matunitlindflem2  34441  poimirlem4  34448  poimirlem20  34464  poimirlem30  34474  broucube  34478  opnmbllem0  34480  areacirclem2  34535  areacirclem4  34537  blssp  34584  sstotbnd2  34605  totbndbnd  34620  prdstotbnd  34625  cnpwstotbnd  34628  heiborlem9  34650  exidcl  34707  exidresid  34710  grpokerinj  34724  iscringd  34829  erim2  35463  prter3  35570  toycom  35661  islfld  35750  lshpsmreu  35797  ldualelvbase  35815  ldualssvscl  35846  lkreqN  35858  lkrlspeqN  35859  erng1lem  37675  erngdvlem4  37679  erng0g  37682  erng1r  37683  erngdvlem4-rN  37687  dva0g  37715  dia1dim2  37750  dia1dimid  37751  dia2dimlem5  37756  dvhelvbasei  37776  dvhvaddass  37785  tendoinvcl  37792  tendolinv  37793  tendorinv  37794  dvhgrp  37795  dvhlveclem  37796  cdlemn4  37886  lcfrlem12N  38242  lcfrlem15  38245  lcdvscl  38293  lcdlssvscl  38294  lcdvsass  38295  lcdvs0N  38304  mapdincl  38349  mapdin  38350  mapdlsmcl  38351  mapdcnvatN  38354  mapdpglem2  38361  mapdpglem12  38371  mapdpglem18  38377  mapdpglem21  38380  mapdpglem22  38381  mapdpglem28  38389  mapdpglem30  38390  hdmaprnlem3N  38538  hdmaprnlem3uN  38539  hdmaprnlem7N  38543  hdmaprnlem8N  38544  hdmaprnlem9N  38545  hdmaprnlem3eN  38546  hdmaprnlem16N  38550  hgmapdcl  38578  hgmapval1  38581  hgmaprnlem4N  38587  hdmapinvlem1  38606  fnsnbt  38671  selvval2lem4  38686  fltnltalem  38792  wepwsolem  39148  kercvrlsm  39189  dfacbasgrp  39214  imo72b2lem0  40022  grurankcld  40087  grumnudlem  40139  grumnud  40140  inaex  40151  gruex  40152  ablsimpg1gend  40184  ablsimpgprmd  40193  dvconstbi  40225  cncmpmax  40849  iooabslt  41337  fmul01lt1lem2  41429  limciccioolb  41465  limcicciooub  41481  limsuppnfdlem  41545  climrescn  41592  climxrrelem  41593  climxrre  41594  liminflimsupxrre  41661  xlimmnfvlem2  41677  xlimpnfvlem2  41681  fsumcncf  41724  ioccncflimc  41731  icocncflimc  41735  cncfiooicclem1  41739  dvbdfbdioolem2  41777  dvnmul  41791  stoweidlem26  41875  stoweidlem34  41883  stoweidlem48  41897  stoweidlem59  41908  dirkercncflem3  41954  fourierdlem32  41988  fourierdlem41  41997  fourierdlem51  42006  fourierdlem63  42018  fourierdlem82  42037  fourierdlem85  42040  fourierdlem93  42048  fourierdlem111  42066  fourierdlem114  42069  etransclem35  42118  hspdifhsp  42462  opnvonmbllem1  42478  ovnovollem1  42502  mbfresmf  42580  smfaddlem1  42603  smfsuplem1  42649  smflimsuplem5  42662  fzoopth  43065  setsidel  43074  setsnidel  43075  prelspr  43152  rnghmsubcsetclem1  43746  rngccatidALTV  43760  zrinitorngc  43771  zrtermorngc  43772  zrzeroorngc  43773  rhmsubcsetclem1  43792  rhmsubcrngclem1  43798  funcringcsetcALTV2lem3  43809  funcringcsetcALTV2lem8  43814  ringccatidALTV  43823  funcringcsetclem3ALTV  43832  funcringcsetclem8ALTV  43837  irinitoringc  43840  zrtermoringc  43841  zrninitoringc  43842  nzerooringczr  43843  srhmsubclem2  43845  srhmsubc  43847  srhmsubcALTVlem1  43863  srhmsubcALTV  43865  rhmsubcALTVlem3  43877  lcosslsp  43995  nnolog2flm1  44153