Theorem eleqtrrd 2868

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-clel 2840

This theorem is referenced by:  3eltr4d  2880  rspc2vd  3903  disjxiun  5101  eldmressnsn  6013  fnsnbg  7152  elimdelov  7496  elovmpt3rab1  7660  fnwelem  8115  tfrlem13  8365  tz7.44-2  8382  omordi  8539  oneo  8554  omeulem2  8556  oeordi  8561  oeeui  8576  nnneo  8629  naddelim  8661  erref  8703  en1uniel  9014  omxpenlem  9054  unblem3  9242  dffi3  9379  ordtypelem10  9477  oismo  9490  cantnff  9631  cantnfp1lem3  9637  cantnflem1  9646  cnfcom  9657  r1ordg  9738  r1pwss  9744  rankwflemb  9753  r1elwf  9756  rankidb  9760  rankonidlem  9788  fseqenlem2  9997  dfac12lem1  10115  dfac12lem2  10116  pwsdompw  10174  ackbij2lem3  10211  ackbij2  10213  cfsmolem  10242  hsmexlem4  10401  ttukeylem3  10483  ttukeylem7  10487  iundom2g  10512  fpwwe2lem8  10611  canthwelem  10623  pwfseqlem4  10635  winalim2  10669  r1wunlim  10710  tskmid  10813  fzopth  13577  predfz  13669  fzoss2  13704  fz1fzo0m1  13727  fzo0addel  13735  fzo0addelr  13736  elfzoext  13739  fzosubel3  13743  elfzomin  13754  elfzonlteqm1  13758  fzoend  13774  fzoopth  13779  fzofzp1  13781  fzofzp1b  13782  peano2fzor  13792  zmodfzo  13915  seqf1olem2  14066  bcn2  14343  swrdccat2  14695  pfxccat1  14727  swrdswrd  14730  pfxccatin12  14758  splfv1  14780  revcl  14786  revlen  14787  revccat  14791  revrev  14792  repswpfx  14810  cshwidxmod  14828  revco  14859  limsupgre  15520  summolem2a  15754  fsumm1  15790  fsumcom2  15813  prodmolem2a  15976  fprodm1  16009  fprodcom2  16026  prmreclem4  16967  prmreclem5  16968  vdwapid1  17023  vdwlem5  17033  vdwlem8  17036  vdwnnlem2  17044  ramub1lem1  17074  ramub1lem2  17075  mrieqvlemd  17673  mreexd  17686  mreexexlemd  17688  catcocl  17729  catass  17730  moni  17781  epii  17788  inviso1  17811  episect  17830  invisoinvl  17835  catsubcat  17884  subccocl  17890  fullsubc  17895  funcco  17916  resf2nd  17940  funcres  17941  fthepi  17975  nati  18003  arwhoma  18090  catccatid  18151  resscatc  18154  catcisolem  18155  catcoppccl  18162  catcfuccl  18163  estrreslem2  18182  funcestrcsetclem3  18186  funcestrcsetclem8  18191  equivestrcsetc  18196  funcsetcestrclem3  18200  funcsetcestrclem8  18206  xpcco  18227  xpcco2  18231  xpccatid  18232  prfcl  18247  catcxpccl  18251  curf12  18271  curf1cl  18272  curf2  18273  curf2cl  18275  curfcl  18276  uncf2  18281  uncfcurf  18283  diag12  18288  diag2  18289  curf2ndf  18291  hofcl  18303  oppchofcl  18304  oyoncl  18314  yonedalem3a  18318  yonedalem4b  18320  yonedalem22  18322  yonedalem3b  18323  yonedalem3  18324  yonedainv  18325  yonffthlem  18326  latcl2  18480  latlem  18481  latjcom  18491  latmcom  18507  clatlem  18546  clatlubcl2  18548  clatglbcl2  18550  acsfiindd  18597  pfxchn  18654  chnind  18665  chnub  18666  chnlt  18667  chnccat  18670  chnrev  18671  gsumpropd2lem  18725  sgrppropd  18777  mndpropd  18805  imasmnd  18821  frmdmnd  18906  frmdgsum  18909  grpsubpropd2  19100  imasgrp  19110  subg0  19186  0ghm  19288  resghm2  19291  ghmco  19294  pwsdiagghm  19302  ghmqusnsglem2  19339  ghmqusnsg  19340  ghmquskerlem2  19343  ghmquskerlem3  19344  ghmqusker  19345  psgnunilem1  19551  psgnunilem5  19552  psgnunilem2  19553  psgnunilem3  19554  sylow1lem4  19659  sylow1lem5  19660  efglem  19774  efgtf  19780  efginvrel2  19785  efginvrel1  19786  efgsdmi  19790  efgs1b  19794  efgsres  19796  efgsfo  19797  efgredleme  19801  efgredlemc  19803  efgredlem  19805  efgcpbllemb  19813  frgp0  19818  frgpadd  19821  frgpinv  19822  vrgpf  19826  vrgpinv  19827  frgpuplem  19830  frgpup1  19833  frgpup2  19834  frgpup3lem  19835  frgpnabllem1  19931  frgpnabllem2  19932  gsumval3  19965  dprdfid  20077  dprdsn  20096  dprd2da  20102  dpjidcl  20118  pgpfac1lem2  20135  pgpfaclem3  20143  ablsimpg1gend  20165  ablsimpgprmd  20175  rngpropd  20240  imasrng  20243  ringpropd  20359  imasring  20400  qusring2  20404  pwsco1rhm  20572  pwsco2rhm  20573  lringuplu  20617  subrgunit  20663  pwsdiagrhm  20680  rnghmsubcsetclem1  20704  zrinitorngc  20715  zrtermorngc  20716  zrzeroorngc  20717  rhmsubcsetclem1  20733  rhmsubcrngclem1  20739  zrtermoringc  20748  zrninitoringc  20749  srhmsubclem2  20751  srhmsubc  20753  cntzsdrg  20871  isabvd  20881  lmodprop2d  21011  islssd  21022  prdsvscacl  21055  prdslmodd  21056  islmhm2  21125  lmhmco  21130  lmhmplusg  21131  lmhmvsca  21132  lmhmpropd  21160  lsppreli  21177  ellspsn4  21214  lssacsex  21234  lspsnat  21235  lidlnsg  21344  qus2idrng  21371  qus1  21372  qusrhm  21374  rhmpreimaidl  21375  rhmqusnsg  21384  rngqiprngghmlem1  21386  rngqiprngfulem1  21410  rhmpreimaprmidl  21436  qsidomlem2  21438  irinitoringc  21586  nzerooringczr  21587  znf1o  21658  cssmre  21800  dsmmlss  21851  frlmsplit2  21880  frlmbas3  21883  frlmup1  21905  assapropd  21978  psr0cl  22059  psrnegcl  22061  psr1cl  22067  resspsrmul  22082  subrgpsr  22084  mvrf  22091  mplmon  22143  mplcoe1  22145  subrgasclcl  22175  mplind  22178  evlslem1  22190  mhmcompl  22229  evlsevl  22240  evlvvval  22241  selvcllem2  22243  subrgply1  22349  psrplusgpropd  22352  ply1coe  22415  cply1coe0bi  22419  lply1binomsc  22428  ply1fermltlchr  22429  evls1val  22437  evls1rhm  22439  evl1val  22446  evl1rhm  22449  pf1ind  22472  evl1scvarpw  22480  evls1fpws  22486  rhmply1  22500  matbas2i  22536  matplusg2  22541  matvsca2  22542  matsubgcell  22548  matvscacell  22550  mpomatmul  22560  mavmulval  22659  mavmulcl  22661  mavmulass  22663  mavmul0  22666  mavmumamul1  22669  m1detdiag  22711  cramerimplem2  22798  mat2pmatmul  22845  mat2pmatlin  22849  monmatcollpw  22893  pmatcollpwfi  22896  mply1topmatcl  22919  pm2mpghm  22930  pm2mpmhmlem2  22933  pm2mp  22939  chpmat1dlem  22949  chpmat1d  22950  chpdmatlem0  22951  chpscmat  22956  chpscmatgsumbin  22958  chpscmatgsummon  22959  chfacfscmulcl  22971  cpmadugsumlemB  22988  cpmadugsumlemC  22989  chcoeffeqlem  22999  cldmreon  23208  neiptopreu  23247  maxlp  23261  ordttopon  23307  ordtrest2lem  23317  cnprcl2  23365  lmcnp  23418  resthauslem  23477  hauscmplem  23520  1stcfb  23559  2ndcctbss  23569  2ndcomap  23572  dis2ndc  23574  loclly  23601  hausllycmp  23608  locfincmp  23640  dissnref  23642  kgeni  23651  kgenidm  23661  ptpjpre2  23694  xkoopn  23703  txopn  23716  ptpjopn  23726  ptcldmpt  23728  ptcls  23730  pthaus  23752  txkgen  23766  xkohaus  23767  xkopt  23769  txconn  23803  imastps  23835  kqid  23842  kqopn  23848  kqcld  23849  isr0  23851  indishmph  23912  pt1hmeo  23920  ptuncnv  23921  ptunhmeo  23922  t0kq  23932  filconn  23997  uzrest  24011  uffixsn  24039  fmfnfmlem2  24069  flimss2  24086  flimss1  24087  flimclslem  24098  flfcnp  24118  fclsfnflim  24141  uffclsflim  24145  fcfelbas  24150  alexsublem  24158  alexsub  24159  cnextcn  24181  cnextfres1  24182  cnextfres  24183  tmdgsum  24209  distgp  24213  indistgp  24214  symgtgp  24220  ghmcnp  24229  qustgpopn  24234  qustgplem  24235  qustgphaus  24237  prdstmdd  24238  prdstgpd  24239  tsmsid  24254  tsmssubm  24257  tsmsmhm  24260  tsmsadd  24261  tsmssplit  24266  utop2nei  24364  utop3cls  24365  neipcfilu  24409  cnextucn  24416  ucnextcn  24417  blpnfctr  24550  lpbl  24617  met2ndci  24636  tmsxps  24650  metcnpi  24658  metcnpi2  24659  metcnpi3  24660  metustid  24668  metustsym  24669  metustexhalf  24670  subgngp  24749  ngptgp  24750  sranlm  24798  nlmvscn  24801  nrginvrcn  24806  lssnlm  24815  nghmcn  24859  iccntr  24936  icccmplem2  24938  msdcn  24956  cncfmptc  25028  cncfmptid  25029  cncfmpt2f  25031  icoopnst  25055  iocopnst  25056  nmoleub2lem3  25231  nmoleub3  25235  nmhmcn  25236  ipcn  25362  cfilfcls  25390  caucfil  25399  equivcau  25416  caubl  25424  flimcfil  25430  cmssmscld  25466  rrxdstprj1  25525  minveclem3b  25544  minveclem4  25548  mulcncf  25562  ovolicc2lem3  25635  ovolicc2lem4  25636  opnmbllem  25717  vitalilem2  25725  mbfsup  25780  mbfinf  25781  mbfi1fseqlem4  25834  limccnp  26007  limccnp2  26008  dvreslem  26025  dvres2lem  26026  dvidlem  26031  dvcnp2  26036  dvcn  26037  dvaddbr  26054  dvmulbr  26055  dvcmul  26060  dvcof  26064  dvcnvlem  26092  dvef  26096  rollelem  26105  dvlip2  26111  dvivthlem1  26124  dvivth  26126  lhop2  26131  lhop  26132  dvcnvrelem1  26133  dvcnvrelem2  26134  dvcnvre  26135  ply1rem  26280  fta1blem  26285  plycpn  26407  plyrem  26423  tayl0  26479  dvtaylp  26487  dvntaylp  26488  dvntaylp0  26489  taylthlem1  26490  taylthlem2  26491  ulmdvlem3  26519  psercn  26543  pserdv  26546  abelth  26558  efabl  26669  efopnlem1  26775  loglesqrt  26880  relogbf  26910  efrlim  27088  dchrghm  27374  dchrptlem3  27384  nodenselem5  27806  nosupres  27825  noinfres  27840  ltslpss  28055  precsexlem11  28364  noseq0  28437  noseqp1  28438  noseqrdgfn  28453  noseqrdgsuc  28455  tgbtwntriv2  28710  tgbtwnne  28713  ercgrg  28740  tgidinside  28794  tgbtwnconn1  28798  tglnne  28851  tglinesseq  28863  tglnne0  28864  tglineneq  28868  ncolncol  28870  coltr3  28872  tglnpt2  28876  tglnpt3  28877  mirln  28903  mirln2  28904  mirconn  28905  krippenlem  28917  footexALT  28945  footexlem1  28946  footexlem2  28947  colperpexlem3  28959  mideulem2  28961  opphllem  28962  oppne3  28970  opphllem1  28974  opphllem2  28975  opphllem4  28977  oppperpex  28980  opphl  28981  hlpasch  28983  hpgerlem  28992  colhp  28997  plngval  29003  lnincplng  29010  plngrotlem1  29013  lnssplnglem  29017  plng3p  29019  midbtwn  29027  lmieu  29032  lmiisolem  29044  sacgr  29079  f1otrg  29125  f1otrge  29126  ebtwntg  29237  ecgrtg  29238  eengtrkg  29241  eengtrkge  29242  upgr1eop  29370  usgredg3  29471  uspgr1eop  29502  usgr1eop  29505  vtxdun  29736  vtxdfiun  29737  1loopgruspgr  29755  1loopgrvd2  29758  1hevtxdg1  29761  1egrvtxdg1  29764  1egrvtxdg0  29766  umgr2v2e  29780  wlkres  29923  wlkp1lem4  29929  wlkp1  29934  cyclnumvtx  30054  wwlksm1edg  30135  wwlksnext  30147  wwlksnextproplem3  30165  clwwlkel  30302  1wlkdlem2  30394  trlsegvdeg  30483  eupth2lem3lem1  30484  eupth2lem3lem2  30485  extwwlkfab  30608  numclwlk2lem2f  30633  spansnid  31820  elspansn4  31830  fnpreimac  32923  ccatf1  33177  ccatws1f1olast  33180  swrdrn2  33182  swrdrn3  33183  swrdf1  33184  splfv3  33186  pwrssmgc  33228  suppgsumssiun  33300  wrdpmtrlast  33321  psgnfzto1stlem  33328  cycpmfv1  33341  cycpmfv2  33342  cycpmco2lem2  33355  cycpmco2lem4  33357  cycpmco2lem5  33358  cycpmco2lem6  33359  cycpmco2  33361  cyc3co2  33368  cycpmrn  33371  submarchi  33414  subrdom  33513  fracfld  33539  imaslmod  33583  quslmod  33588  quslmhm  33589  nsgqusf1olem2  33634  lmhmqusker  33637  rhmquskerlem  33644  idlinsubrg  33650  drngidl  33652  mxidlprm  33665  opprmxidlabs  33681  qsdrngilem  33688  qsdrngi  33689  qsdrnglem2  33690  idlsrg0g  33708  pidufd  33745  dfufd2lem  33751  fply1  33760  evl1fpws  33766  ressply1evls1  33767  ressply1sub  33772  ply1asclunit  33776  r1plmhm  33811  0mplrim  33816  selvascl  33819  selvply1rhmlema  33820  selvply1rhmlem1  33822  extvfvcl  33838  evlextv  33844  mplvrpmga  33847  psrmon  33851  psrmonprod  33854  mplmonprod  33856  issply  33863  esplympl  33869  esplyind  33877  drgextlsp  33896  matdim  33917  ply1degltdimlem  33924  lindsunlem  33926  qusdimsum  33930  fedgmullem1  33931  fedgmullem2  33932  fedgmul  33933  extdg1id  33968  evls1fldgencl  33972  irngss  33989  irngnzply1  33993  extdgfialglem1  33994  extdgfialglem2  33995  minplymindeg  34010  minplyirredlem  34012  irredminply  34018  algextdeglem2  34020  constrconj  34047  constrfiss  34053  1smat1  34106  submat1n  34107  lmatfval  34116  lmatcl  34118  mdetpmtr1  34125  madjusmdetlem4  34132  qtopt1  34137  qtophaus  34138  locfinref  34143  zarcls1  34171  zarclsiin  34173  zarmxt1  34182  zarcmplem  34183  rhmpreimacn  34187  ordtrest2NEWlem  34224  elzrhunit  34279  qqhcn  34293  qqhucn  34294  esumel  34349  esumsplit  34355  sigagenss2  34452  elsx  34496  sxbrsigalem0  34573  dya2icoseg  34579  eulerpartlemb  34670  eulerpartlemgvv  34678  iwrdsplit  34689  sseqfv2  34696  probfinmeasb  34730  dstrvprob  34774  dstfrvel  34776  ballotlemrv  34822  signstfvn  34868  signstfvp  34870  signstfveq0  34876  signsvtp  34882  signsvtn  34883  reprsuc  34914  reprpmtf1o  34925  morleylemrneab  34970  lpadleft  34985  bnj1006  35260  bnj1018g  35263  bnj1018  35264  bnj1121  35285  bnj1398  35334  bnj1450  35350  bnj1501  35367  revpfxsfxrev  35473  swrdrevpfx  35474  pfxwlk  35482  revwlk  35483  swrdwlk  35485  subfacp1lem5  35542  ptpconn  35591  indispconn  35592  cvxsconn  35601  cvmseu  35634  cvmliftmolem2  35640  cvmliftlem7  35649  cvmliftlem10  35652  cvmliftlem13  35654  cvmlift2lem12  35672  satfv1lem  35720  satffunlem1lem2  35761  satffunlem2lem2  35764  satefvfmla1  35783  mrsubcv  35868  mrsubff  35870  mrsubrn  35871  mrsubccat  35876  elmrsubrn  35878  mrsubco  35879  mrsubvrs  35880  mvhf  35916  msubvrs  35918  mclsax  35927  r1peuqusdeg1  36001  linerflx1  36507  linerflx2  36509  fwddifnval  36521  elhf2  36533  neibastop2lem  36728  weiunpo  36833  weiunso  36834  icoreunrn  37860  relowlssretop  37864  sucneqond  37866  matunitlindflem2  38123  poimirlem4  38130  poimirlem20  38146  poimirlem30  38156  broucube  38160  opnmbllem0  38162  areacirclem2  38215  areacirclem4  38217  blssp  38262  sstotbnd2  38280  totbndbnd  38295  prdstotbnd  38300  cnpwstotbnd  38303  heiborlem9  38325  exidcl  38382  exidresid  38385  grpokerinj  38399  iscringd  38504  erimeq2  39269  prter3  39513  toycom  39604  islfld  39693  lshpsmreu  39740  ldualelvbase  39758  ldualssvscl  39789  lkreqN  39801  lkrlspeqN  39802  erng1lem  41618  erngdvlem4  41622  erng0g  41625  erng1r  41626  erngdvlem4-rN  41630  dva0g  41658  dia1dim2  41693  dia1dimid  41694  dia2dimlem5  41699  dvhelvbasei  41719  dvhvaddass  41728  tendoinvcl  41735  tendolinv  41736  tendorinv  41737  dvhgrp  41738  dvhlveclem  41739  cdlemn4  41829  lcfrlem12N  42185  lcfrlem15  42188  lcdvscl  42236  lcdlssvscl  42237  lcdvsass  42238  lcdvs0N  42247  mapdincl  42292  mapdin  42293  mapdlsmcl  42294  mapdcnvatN  42297  mapdpglem2  42304  mapdpglem12  42314  mapdpglem18  42320  mapdpglem21  42323  mapdpglem22  42324  mapdpglem28  42332  mapdpglem30  42333  hdmaprnlem3N  42481  hdmaprnlem3uN  42482  hdmaprnlem7N  42486  hdmaprnlem8N  42487  hdmaprnlem9N  42488  hdmaprnlem3eN  42489  hdmaprnlem16N  42493  hgmapdcl  42521  hgmapval1  42524  hgmaprnlem4N  42530  hdmapinvlem1  42549  fzadd2d  42603  aks6d1c2lem4  42751  sticksstones1  42770  sticksstones8  42777  sticksstones9  42778  sticksstones10  42779  sticksstones11  42780  sticksstones17  42787  sticksstones18  42788  aks6d1c6lem4  42797  rhmqusspan  42809  aks5lem2  42811  mhmcopsr  43169  evlsbagval  43175  evlvvvallem  43176  evlselv  43178  mhpind  43183  fltnltalem  43251  wepwsolem  43626  kercvrlsm  43667  dfacbasgrp  43692  onexomgt  43825  onexoegt  43828  onov0suclim  43858  cantnftermord  43904  cantnf2  43909  omcl2  43917  ofoaf  43939  ofoafo  43940  grurankcld  44816  grumnudlem  44854  grumnud  44855  inaex  44866  gruex  44867  dvconstbi  44903  cncmpmax  45611  iooabslt  46074  fmul01lt1lem2  46160  limciccioolb  46196  limcicciooub  46210  limsuppnfdlem  46274  climrescn  46321  climxrrelem  46322  climxrre  46323  liminflimsupxrre  46390  xlimmnfvlem2  46406  xlimpnfvlem2  46410  fsumcncf  46451  ioccncflimc  46458  cncfuni  46459  icocncflimc  46462  cncfiooicclem1  46466  dvbdfbdioolem2  46502  dvnmul  46516  dvnprodlem1  46519  stoweidlem26  46599  stoweidlem34  46607  stoweidlem48  46621  stoweidlem59  46632  dirkercncflem3  46678  fourierdlem32  46712  fourierdlem41  46721  fourierdlem51  46730  fourierdlem63  46742  fourierdlem82  46761  fourierdlem85  46764  fourierdlem93  46772  fourierdlem111  46790  fourierdlem114  46793  etransclem35  46842  hoicvr  47121  hspdifhsp  47189  opnvonmbllem1  47205  ovnovollem1  47229  mbfresmf  47312  smfaddlem1  47336  smfsuplem1  47384  smflimsuplem5  47397  chnerlem2  47458  setsidel  47981  setsnidel  47982  imasetpreimafvbijlemf  48006  prelspr  48091  upgrimpths  48530  gpgprismgr4cycllem9  48724  rngccatidALTV  48893  rhmsubcALTVlem3  48904  funcringcsetcALTV2lem3  48913  funcringcsetcALTV2lem8  48918  ringccatidALTV  48927  funcringcsetclem3ALTV  48936  funcringcsetclem8ALTV  48941  srhmsubcALTVlem1  48944  srhmsubcALTV  48946  lcosslsp  49070  nnolog2flm1  49222  ffvbr  49486  glbprlem  49595  topdlat  49634  catprs  49641  iinfsubc  49688  iinfconstbaslem  49695  imaid  49784  fthcomf  49787  uptr2  49851  natoppf2  49860  natoppfb  49861  swapf2  49904  swapfiso  49915  swapciso  49916  oppc1stflem  49917  cofuswapf2  49925  fuco22natlem  49975  fucoppcffth  50041  oppcthinco  50069  oppcthinendcALT  50071  thinccisod  50084  termco  50111  termchommo  50115  termcid  50116  termcterm  50143  termcterm2  50144  diagciso  50169  diagcic  50170  funcsn  50171  uobeqterm  50176  mndtccatid  50217  grptcmon  50223  grptcepi  50224  2arwcat  50230  lanval2  50257  ranval2  50260  lanup  50271  ranup  50272  lmddu  50297