Theorem eleqtrrd 2836

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 2744	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrd 2835	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 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2730  df-clel 2811

This theorem is referenced by:  3eltr4d  2848  rspc2vd  3839  disjxiun  5027  eldmressnsn  5868  elimdelov  7264  elovmpt3rab1  7421  fnwelem  7851  tfrlem13  8055  tz7.44-2  8072  omordi  8223  oneo  8238  omeulem2  8240  oeordi  8244  oeeui  8259  nnneo  8309  erref  8340  en1uniel  8628  omxpenlem  8667  unblem3  8846  dffi3  8968  ordtypelem10  9064  oismo  9077  cantnff  9210  cantnfp1lem3  9216  cantnflem1  9225  cnfcom  9236  r1ordg  9280  r1pwss  9286  rankwflemb  9295  r1elwf  9298  rankidb  9302  rankonidlem  9330  fseqenlem2  9525  dfac12lem1  9643  dfac12lem2  9644  pwsdompw  9704  ackbij2lem3  9741  ackbij2  9743  cfsmolem  9770  hsmexlem4  9929  ttukeylem3  10011  ttukeylem7  10015  iundom2g  10040  fpwwe2lem8  10138  canthwelem  10150  pwfseqlem4  10162  winalim2  10196  r1wunlim  10237  tskmid  10340  fzopth  13035  predfz  13123  fzoss2  13156  fz1fzo0m1  13176  fzo0addel  13182  fzo0addelr  13183  fzosubel3  13189  elfzomin  13200  elfzonlteqm1  13204  fzoend  13219  fzofzp1  13225  fzofzp1b  13226  peano2fzor  13235  zmodfzo  13353  seqf1olem2  13502  bcn2  13771  swrdccat2  14120  pfxccat1  14153  swrdswrd  14156  pfxccatin12  14184  splfv1  14206  revcl  14212  revlen  14213  revccat  14217  revrev  14218  repswpfx  14236  cshwidxmod  14254  revco  14285  limsupgre  14928  summolem2a  15165  fsumm1  15199  fsumcom2  15222  prodmolem2a  15380  fprodm1  15413  fprodcom2  15430  prmreclem4  16355  prmreclem5  16356  vdwapid1  16411  vdwlem5  16421  vdwlem8  16424  vdwnnlem2  16432  ramub1lem1  16462  ramub1lem2  16463  mrieqvlemd  17003  mreexd  17016  mreexexlemd  17018  catcocl  17059  catass  17060  moni  17111  epii  17118  inviso1  17141  episect  17160  invisoinvl  17165  catsubcat  17214  subccocl  17220  fullsubc  17225  funcco  17246  resf2nd  17270  funcres  17271  fthepi  17303  nati  17330  arwhoma  17417  catccatid  17478  resscatc  17481  catcisolem  17482  catcoppccl  17484  catcfuccl  17485  estrreslem2  17504  funcestrcsetclem3  17508  funcestrcsetclem8  17513  equivestrcsetc  17518  funcsetcestrclem3  17522  funcsetcestrclem8  17528  xpcco  17549  xpcco2  17553  xpccatid  17554  prfcl  17569  catcxpccl  17573  curf12  17593  curf1cl  17594  curf2  17595  curf2cl  17597  curfcl  17598  uncf2  17603  uncfcurf  17605  diag12  17610  diag2  17611  curf2ndf  17613  hofcl  17625  oppchofcl  17626  oyoncl  17636  yonedalem3a  17640  yonedalem4b  17642  yonedalem22  17644  yonedalem3b  17645  yonedalem3  17646  yonedainv  17647  yonffthlem  17648  latcl2  17774  latlem  17775  latjcom  17785  latmcom  17801  clatlem  17837  clatlubcl2  17839  clatglbcl2  17841  acsfiindd  17903  gsumpropd2lem  18005  mndpropd  18052  imasmnd  18065  frmdmnd  18140  frmdgsum  18143  grpsubpropd2  18323  imasgrp  18333  subg0  18403  0ghm  18490  resghm2  18493  ghmco  18496  pwsdiagghm  18504  psgnunilem1  18739  psgnunilem5  18740  psgnunilem2  18741  psgnunilem3  18742  sylow1lem4  18844  sylow1lem5  18845  efglem  18960  efgtf  18966  efginvrel2  18971  efginvrel1  18972  efgsdmi  18976  efgs1b  18980  efgsres  18982  efgsfo  18983  efgredleme  18987  efgredlemc  18989  efgredlem  18991  efgcpbllemb  18999  frgp0  19004  frgpadd  19007  frgpinv  19008  vrgpf  19012  vrgpinv  19013  frgpuplem  19016  frgpup1  19019  frgpup2  19020  frgpup3lem  19021  frgpnabllem1  19112  frgpnabllem2  19113  gsumval3  19146  dprdfid  19258  dprdsn  19277  dprd2da  19283  dpjidcl  19299  pgpfac1lem2  19316  pgpfaclem3  19324  ablsimpg1gend  19346  ablsimpgprmd  19356  ringpropd  19454  imasring  19491  qusring2  19492  pwsco1rhm  19612  pwsco2rhm  19613  subrgunit  19672  pwsdiagrhm  19688  cntzsdrg  19700  isabvd  19710  lmodprop2d  19815  islssd  19826  prdsvscacl  19859  prdslmodd  19860  islmhm2  19929  lmhmco  19934  lmhmplusg  19935  lmhmvsca  19936  lmhmpropd  19964  lsppreli  19981  lspsnel4  20015  lssacsex  20035  lspsnat  20036  qus1  20127  qusrhm  20129  znf1o  20370  cssmre  20509  dsmmlss  20560  frlmsplit2  20589  frlmbas3  20592  frlmup1  20614  assapropd  20685  psr0cl  20773  psrnegcl  20775  psr1cl  20781  resspsrmul  20796  subrgpsr  20798  mvrf  20803  mplmon  20846  mplcoe1  20848  subrgasclcl  20879  mplind  20882  evlslem1  20896  subrgply1  21008  psrplusgpropd  21011  ply1coe  21071  cply1coe0bi  21075  lply1binomsc  21082  evls1val  21090  evls1rhm  21092  evl1val  21099  evl1rhm  21102  pf1ind  21125  evl1scvarpw  21133  matbas2i  21173  matplusg2  21178  matvsca2  21179  matsubgcell  21185  matvscacell  21187  mpomatmul  21197  mavmulval  21296  mavmulcl  21298  mavmulass  21300  mavmul0  21303  mavmumamul1  21306  m1detdiag  21348  cramerimplem2  21435  mat2pmatmul  21482  mat2pmatlin  21486  monmatcollpw  21530  pmatcollpwfi  21533  mply1topmatcl  21556  pm2mpghm  21567  pm2mpmhmlem2  21570  pm2mp  21576  chpmat1dlem  21586  chpmat1d  21587  chpdmatlem0  21588  chpscmat  21593  chpscmatgsumbin  21595  chpscmatgsummon  21596  chfacfscmulcl  21608  cpmadugsumlemB  21625  cpmadugsumlemC  21626  chcoeffeqlem  21636  cldmreon  21845  neiptopreu  21884  maxlp  21898  ordttopon  21944  ordtrest2lem  21954  cnprcl2  22002  lmcnp  22055  resthauslem  22114  hauscmplem  22157  1stcfb  22196  2ndcctbss  22206  2ndcomap  22209  dis2ndc  22211  loclly  22238  hausllycmp  22245  locfincmp  22277  dissnref  22279  kgeni  22288  kgenidm  22298  ptpjpre2  22331  xkoopn  22340  txopn  22353  ptpjopn  22363  ptcldmpt  22365  ptcls  22367  pthaus  22389  txkgen  22403  xkohaus  22404  xkopt  22406  txconn  22440  imastps  22472  kqid  22479  kqopn  22485  kqcld  22486  isr0  22488  indishmph  22549  pt1hmeo  22557  ptuncnv  22558  ptunhmeo  22559  t0kq  22569  filconn  22634  uzrest  22648  uffixsn  22676  fmfnfmlem2  22706  flimss2  22723  flimss1  22724  flimclslem  22735  flfcnp  22755  fclsfnflim  22778  uffclsflim  22782  fcfelbas  22787  alexsublem  22795  alexsub  22796  cnextcn  22818  cnextfres1  22819  cnextfres  22820  tmdgsum  22846  distgp  22850  indistgp  22851  symgtgp  22857  ghmcnp  22866  qustgpopn  22871  qustgplem  22872  qustgphaus  22874  prdstmdd  22875  prdstgpd  22876  tsmsid  22891  tsmssubm  22894  tsmsmhm  22897  tsmsadd  22898  tsmssplit  22903  utop2nei  23002  utop3cls  23003  neipcfilu  23048  cnextucn  23055  ucnextcn  23056  blpnfctr  23189  lpbl  23256  met2ndci  23275  tmsxps  23289  metcnpi  23297  metcnpi2  23298  metcnpi3  23299  metustid  23307  metustsym  23308  metustexhalf  23309  subgngp  23388  ngptgp  23389  sranlm  23437  nlmvscn  23440  nrginvrcn  23445  lssnlm  23454  nghmcn  23498  iccntr  23573  icccmplem2  23575  msdcn  23593  cncfmptc  23664  cncfmptid  23665  cncfmpt2f  23667  icoopnst  23691  iocopnst  23692  nmoleub2lem3  23867  nmoleub3  23871  nmhmcn  23872  ipcn  23998  cfilfcls  24026  caucfil  24035  equivcau  24052  caubl  24060  flimcfil  24066  cmssmscld  24102  rrxdstprj1  24161  minveclem3b  24180  minveclem4  24184  ovolicc2lem3  24271  ovolicc2lem4  24272  opnmbllem  24353  vitalilem2  24361  mbfsup  24416  mbfinf  24417  mbfi1fseqlem4  24471  limccnp  24643  limccnp2  24644  dvreslem  24661  dvres2lem  24662  dvidlem  24667  dvcnp2  24672  dvcn  24673  dvaddbr  24690  dvmulbr  24691  dvcmul  24696  dvcof  24700  dvcnvlem  24728  dvef  24732  rollelem  24741  dvlip2  24747  dvivthlem1  24760  dvivth  24762  lhop2  24767  lhop  24768  dvcnvrelem1  24769  dvcnvrelem2  24770  dvcnvre  24771  ply1rem  24916  fta1blem  24921  plycpn  25037  plyrem  25053  tayl0  25109  dvtaylp  25117  dvntaylp  25118  dvntaylp0  25119  taylthlem1  25120  taylthlem2  25121  ulmdvlem3  25149  psercn  25173  pserdv  25176  abelth  25188  efabl  25294  efopnlem1  25399  loglesqrt  25499  relogbf  25529  efrlim  25707  dchrghm  25992  dchrptlem3  26002  tgbtwntriv2  26433  tgbtwnne  26436  ercgrg  26463  tgidinside  26517  tgbtwnconn1  26521  tglnne  26574  tglnne0  26586  tglnpt2  26587  tglineneq  26590  ncolncol  26592  coltr3  26594  mirln  26622  mirln2  26623  mirconn  26624  krippenlem  26636  footexALT  26664  footexlem1  26665  footexlem2  26666  colperpexlem3  26678  mideulem2  26680  opphllem  26681  oppne3  26689  opphllem1  26693  opphllem2  26694  opphllem4  26696  oppperpex  26699  opphl  26700  hlpasch  26702  hpgerlem  26711  colhp  26716  midbtwn  26725  lmieu  26730  lmiisolem  26742  sacgr  26777  f1otrg  26817  f1otrge  26818  ebtwntg  26928  ecgrtg  26929  eengtrkg  26932  eengtrkge  26933  upgr1eop  27060  usgredg3  27158  uspgr1eop  27189  usgr1eop  27192  vtxdun  27423  vtxdfiun  27424  1loopgruspgr  27442  1loopgrvd2  27445  1hevtxdg1  27448  1egrvtxdg1  27451  1egrvtxdg0  27453  umgr2v2e  27467  wlkres  27612  wlkp1lem4  27618  wlkp1  27623  wwlksm1edg  27819  wwlksnext  27831  wwlksnextproplem3  27849  clwwlkel  27983  1wlkdlem2  28075  trlsegvdeg  28164  eupth2lem3lem1  28165  eupth2lem3lem2  28166  extwwlkfab  28289  numclwlk2lem2f  28314  spansnid  29498  elspansn4  29508  fnpreimac  30583  ccatf1  30798  swrdrn2  30801  swrdrn3  30802  swrdf1  30803  splfv3  30805  pwrssmgc  30855  psgnfzto1stlem  30944  cycpmfv1  30957  cycpmfv2  30958  cycpmco2lem2  30971  cycpmco2lem4  30973  cycpmco2lem5  30974  cycpmco2lem6  30975  cycpmco2  30977  cyc3co2  30984  cycpmrn  30987  submarchi  31017  imaslmod  31125  quslmod  31126  quslmhm  31127  nsgqusf1olem2  31171  rhmpreimaidl  31175  idlinsubrg  31180  lidlnsg  31193  rhmpreimaprmidl  31199  qsidomlem2  31201  mxidlprm  31212  idlsrg0g  31223  fply1  31239  ply1fermltl  31242  drgextlsp  31253  matdim  31270  lindsunlem  31277  qusdimsum  31281  fedgmullem1  31282  fedgmullem2  31283  fedgmul  31284  extdg1id  31310  1smat1  31326  submat1n  31327  lmatfval  31336  lmatcl  31338  mdetpmtr1  31345  madjusmdetlem4  31352  qtopt1  31357  qtophaus  31358  locfinref  31363  zarcls1  31391  zarclsiin  31393  zarmxt1  31402  zarcmplem  31403  rhmpreimacn  31407  ordtrest2NEWlem  31444  elzrhunit  31499  qqhcn  31511  qqhucn  31512  esumel  31585  esumsplit  31591  sigagenss2  31688  elsx  31732  sxbrsigalem0  31808  dya2icoseg  31814  eulerpartlemb  31905  eulerpartlemgvv  31913  iwrdsplit  31924  sseqfv2  31931  probfinmeasb  31965  dstrvprob  32008  dstfrvel  32010  ballotlemrv  32056  signstfvn  32118  signstfvp  32120  signstfveq0  32126  signsvtp  32132  signsvtn  32133  reprsuc  32165  reprpmtf1o  32176  lpadleft  32233  bnj1006  32511  bnj1018g  32514  bnj1018  32515  bnj1121  32536  bnj1398  32585  bnj1450  32601  bnj1501  32618  revpfxsfxrev  32648  swrdrevpfx  32649  pfxwlk  32656  revwlk  32657  swrdwlk  32659  subfacp1lem5  32717  ptpconn  32766  indispconn  32767  cvxsconn  32776  cvmseu  32809  cvmliftmolem2  32815  cvmliftlem7  32824  cvmliftlem10  32827  cvmliftlem13  32829  cvmlift2lem12  32847  satfv1lem  32895  satffunlem1lem2  32936  satffunlem2lem2  32939  satefvfmla1  32958  mrsubcv  33043  mrsubff  33045  mrsubrn  33046  mrsubccat  33051  elmrsubrn  33053  mrsubco  33054  mrsubvrs  33055  mvhf  33091  msubvrs  33093  mclsax  33102  naddelim  33479  nodenselem5  33532  nosupres  33551  noinfres  33566  sltlpss  33725  linerflx1  34089  linerflx2  34091  fwddifnval  34103  elhf2  34115  neibastop2lem  34187  icoreunrn  35153  relowlssretop  35157  sucneqond  35159  matunitlindflem2  35397  poimirlem4  35404  poimirlem20  35420  poimirlem30  35430  broucube  35434  opnmbllem0  35436  areacirclem2  35489  areacirclem4  35491  blssp  35537  sstotbnd2  35555  totbndbnd  35570  prdstotbnd  35575  cnpwstotbnd  35578  heiborlem9  35600  exidcl  35657  exidresid  35660  grpokerinj  35674  iscringd  35779  erim2  36412  prter3  36519  toycom  36610  islfld  36699  lshpsmreu  36746  ldualelvbase  36764  ldualssvscl  36795  lkreqN  36807  lkrlspeqN  36808  erng1lem  38624  erngdvlem4  38628  erng0g  38631  erng1r  38632  erngdvlem4-rN  38636  dva0g  38664  dia1dim2  38699  dia1dimid  38700  dia2dimlem5  38705  dvhelvbasei  38725  dvhvaddass  38734  tendoinvcl  38741  tendolinv  38742  tendorinv  38743  dvhgrp  38744  dvhlveclem  38745  cdlemn4  38835  lcfrlem12N  39191  lcfrlem15  39194  lcdvscl  39242  lcdlssvscl  39243  lcdvsass  39244  lcdvs0N  39253  mapdincl  39298  mapdin  39299  mapdlsmcl  39300  mapdcnvatN  39303  mapdpglem2  39310  mapdpglem12  39320  mapdpglem18  39326  mapdpglem21  39329  mapdpglem22  39330  mapdpglem28  39338  mapdpglem30  39339  hdmaprnlem3N  39487  hdmaprnlem3uN  39488  hdmaprnlem7N  39492  hdmaprnlem8N  39493  hdmaprnlem9N  39494  hdmaprnlem3eN  39495  hdmaprnlem16N  39499  hgmapdcl  39527  hgmapval1  39530  hgmaprnlem4N  39536  hdmapinvlem1  39555  fzadd2d  39606  sticksstones1  39708  sticksstones8  39715  fnsnbt  39790  selvval2lem2  39807  selvval2lem4  39810  evlsbagval  39854  mhpind  39862  mhphf  39864  fltnltalem  40071  wepwsolem  40439  kercvrlsm  40480  dfacbasgrp  40505  imo72b2lem0  41322  grurankcld  41393  grumnudlem  41445  grumnud  41446  inaex  41457  gruex  41458  dvconstbi  41490  cncmpmax  42113  iooabslt  42577  fmul01lt1lem2  42668  limciccioolb  42704  limcicciooub  42720  limsuppnfdlem  42784  climrescn  42831  climxrrelem  42832  climxrre  42833  liminflimsupxrre  42900  xlimmnfvlem2  42916  xlimpnfvlem2  42920  fsumcncf  42961  ioccncflimc  42968  icocncflimc  42972  cncfiooicclem1  42976  dvbdfbdioolem2  43012  dvnmul  43026  stoweidlem26  43109  stoweidlem34  43117  stoweidlem48  43131  stoweidlem59  43142  dirkercncflem3  43188  fourierdlem32  43222  fourierdlem41  43231  fourierdlem51  43240  fourierdlem63  43252  fourierdlem82  43271  fourierdlem85  43274  fourierdlem93  43282  fourierdlem111  43300  fourierdlem114  43303  etransclem35  43352  hspdifhsp  43696  opnvonmbllem1  43712  ovnovollem1  43736  mbfresmf  43814  smfaddlem1  43837  smfsuplem1  43883  smflimsuplem5  43896  fzoopth  44353  setsidel  44362  setsnidel  44363  imasetpreimafvbijlemf  44387  prelspr  44472  rnghmsubcsetclem1  45067  rngccatidALTV  45081  zrinitorngc  45092  zrtermorngc  45093  zrzeroorngc  45094  rhmsubcsetclem1  45113  rhmsubcrngclem1  45119  funcringcsetcALTV2lem3  45130  funcringcsetcALTV2lem8  45135  ringccatidALTV  45144  funcringcsetclem3ALTV  45153  funcringcsetclem8ALTV  45158  irinitoringc  45161  zrtermoringc  45162  zrninitoringc  45163  nzerooringczr  45164  srhmsubclem2  45166  srhmsubc  45168  srhmsubcALTVlem1  45184  srhmsubcALTV  45186  rhmsubcALTVlem3  45198  lcosslsp  45313  nnolog2flm1  45470  catprs  45773  mndtccatid  45827  grptcmon  45830  grptcepi  45831