Theorem eleqtrrd 2834

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  3eltr4d  2846  rspc2vd  3893  disjxiun  5086  eldmressnsn  5972  fnsnbg  7098  elimdelov  7442  elovmpt3rab1  7606  fnwelem  8061  tfrlem13  8309  tz7.44-2  8326  omordi  8481  oneo  8496  omeulem2  8498  oeordi  8502  oeeui  8517  nnneo  8570  naddelim  8601  erref  8642  en1uniel  8951  omxpenlem  8991  unblem3  9178  dffi3  9315  ordtypelem10  9413  oismo  9426  cantnff  9564  cantnfp1lem3  9570  cantnflem1  9579  cnfcom  9590  r1ordg  9671  r1pwss  9677  rankwflemb  9686  r1elwf  9689  rankidb  9693  rankonidlem  9721  fseqenlem2  9916  dfac12lem1  10035  dfac12lem2  10036  pwsdompw  10094  ackbij2lem3  10131  ackbij2  10133  cfsmolem  10161  hsmexlem4  10320  ttukeylem3  10402  ttukeylem7  10406  iundom2g  10431  fpwwe2lem8  10529  canthwelem  10541  pwfseqlem4  10553  winalim2  10587  r1wunlim  10628  tskmid  10731  fzopth  13461  predfz  13553  fzoss2  13587  fz1fzo0m1  13610  fzo0addel  13618  fzo0addelr  13619  elfzoext  13622  fzosubel3  13626  elfzomin  13637  elfzonlteqm1  13641  fzoend  13657  fzoopth  13662  fzofzp1  13664  fzofzp1b  13665  peano2fzor  13675  zmodfzo  13798  seqf1olem2  13949  bcn2  14226  swrdccat2  14577  pfxccat1  14609  swrdswrd  14612  pfxccatin12  14640  splfv1  14662  revcl  14668  revlen  14669  revccat  14673  revrev  14674  repswpfx  14692  cshwidxmod  14710  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  pfxchn  18516  chnind  18527  chnub  18528  chnlt  18529  chnccat  18532  chnrev  18533  gsumpropd2lem  18587  sgrppropd  18639  mndpropd  18667  imasmnd  18683  frmdmnd  18767  frmdgsum  18770  grpsubpropd2  18959  imasgrp  18969  subg0  19045  0ghm  19142  resghm2  19145  ghmco  19148  pwsdiagghm  19156  ghmqusnsglem2  19193  ghmqusnsg  19194  ghmquskerlem2  19197  ghmquskerlem3  19198  ghmqusker  19199  psgnunilem1  19405  psgnunilem5  19406  psgnunilem2  19407  psgnunilem3  19408  sylow1lem4  19513  sylow1lem5  19514  efglem  19628  efgtf  19634  efginvrel2  19639  efginvrel1  19640  efgsdmi  19644  efgs1b  19648  efgsres  19650  efgsfo  19651  efgredleme  19655  efgredlemc  19657  efgredlem  19659  efgcpbllemb  19667  frgp0  19672  frgpadd  19675  frgpinv  19676  vrgpf  19680  vrgpinv  19681  frgpuplem  19684  frgpup1  19687  frgpup2  19688  frgpup3lem  19689  frgpnabllem1  19785  frgpnabllem2  19786  gsumval3  19819  dprdfid  19931  dprdsn  19950  dprd2da  19956  dpjidcl  19972  pgpfac1lem2  19989  pgpfaclem3  19997  ablsimpg1gend  20019  ablsimpgprmd  20029  rngpropd  20092  imasrng  20095  ringpropd  20206  imasring  20248  qusring2  20252  pwsco1rhm  20417  pwsco2rhm  20418  lringuplu  20459  subrgunit  20505  pwsdiagrhm  20522  rnghmsubcsetclem1  20546  zrinitorngc  20557  zrtermorngc  20558  zrzeroorngc  20559  rhmsubcsetclem1  20575  rhmsubcrngclem1  20581  zrtermoringc  20590  zrninitoringc  20591  srhmsubclem2  20593  srhmsubc  20595  cntzsdrg  20717  isabvd  20727  lmodprop2d  20857  islssd  20868  prdsvscacl  20901  prdslmodd  20902  islmhm2  20972  lmhmco  20977  lmhmplusg  20978  lmhmvsca  20979  lmhmpropd  21007  lsppreli  21024  ellspsn4  21061  lssacsex  21081  lspsnat  21082  lidlnsg  21185  qus2idrng  21210  qus1  21211  qusrhm  21213  rhmpreimaidl  21214  rhmqusnsg  21222  rngqiprngghmlem1  21224  rngqiprngfulem1  21248  irinitoringc  21416  nzerooringczr  21417  znf1o  21488  cssmre  21630  dsmmlss  21681  frlmsplit2  21710  frlmbas3  21713  frlmup1  21735  assapropd  21809  psr0cl  21889  psrnegcl  21891  psr1cl  21898  resspsrmul  21913  subrgpsr  21915  mvrf  21922  mplmon  21970  mplcoe1  21972  subrgasclcl  22002  mplind  22005  evlslem1  22017  subrgply1  22145  psrplusgpropd  22148  ply1coe  22213  cply1coe0bi  22217  lply1binomsc  22226  ply1fermltlchr  22227  evls1val  22235  evls1rhm  22237  evl1val  22244  evl1rhm  22247  pf1ind  22270  evl1scvarpw  22278  evls1fpws  22284  mhmcompl  22295  rhmply1  22301  matbas2i  22337  matplusg2  22342  matvsca2  22343  matsubgcell  22349  matvscacell  22351  mpomatmul  22361  mavmulval  22460  mavmulcl  22462  mavmulass  22464  mavmul0  22467  mavmumamul1  22470  m1detdiag  22512  cramerimplem2  22599  mat2pmatmul  22646  mat2pmatlin  22650  monmatcollpw  22694  pmatcollpwfi  22697  mply1topmatcl  22720  pm2mpghm  22731  pm2mpmhmlem2  22734  pm2mp  22740  chpmat1dlem  22750  chpmat1d  22751  chpdmatlem0  22752  chpscmat  22757  chpscmatgsumbin  22759  chpscmatgsummon  22760  chfacfscmulcl  22772  cpmadugsumlemB  22789  cpmadugsumlemC  22790  chcoeffeqlem  22800  cldmreon  23009  neiptopreu  23048  maxlp  23062  ordttopon  23108  ordtrest2lem  23118  cnprcl2  23166  lmcnp  23219  resthauslem  23278  hauscmplem  23321  1stcfb  23360  2ndcctbss  23370  2ndcomap  23373  dis2ndc  23375  loclly  23402  hausllycmp  23409  locfincmp  23441  dissnref  23443  kgeni  23452  kgenidm  23462  ptpjpre2  23495  xkoopn  23504  txopn  23517  ptpjopn  23527  ptcldmpt  23529  ptcls  23531  pthaus  23553  txkgen  23567  xkohaus  23568  xkopt  23570  txconn  23604  imastps  23636  kqid  23643  kqopn  23649  kqcld  23650  isr0  23652  indishmph  23713  pt1hmeo  23721  ptuncnv  23722  ptunhmeo  23723  t0kq  23733  filconn  23798  uzrest  23812  uffixsn  23840  fmfnfmlem2  23870  flimss2  23887  flimss1  23888  flimclslem  23899  flfcnp  23919  fclsfnflim  23942  uffclsflim  23946  fcfelbas  23951  alexsublem  23959  alexsub  23960  cnextcn  23982  cnextfres1  23983  cnextfres  23984  tmdgsum  24010  distgp  24014  indistgp  24015  symgtgp  24021  ghmcnp  24030  qustgpopn  24035  qustgplem  24036  qustgphaus  24038  prdstmdd  24039  prdstgpd  24040  tsmsid  24055  tsmssubm  24058  tsmsmhm  24061  tsmsadd  24062  tsmssplit  24067  utop2nei  24165  utop3cls  24166  neipcfilu  24210  cnextucn  24217  ucnextcn  24218  blpnfctr  24351  lpbl  24418  met2ndci  24437  tmsxps  24451  metcnpi  24459  metcnpi2  24460  metcnpi3  24461  metustid  24469  metustsym  24470  metustexhalf  24471  subgngp  24550  ngptgp  24551  sranlm  24599  nlmvscn  24602  nrginvrcn  24607  lssnlm  24616  nghmcn  24660  iccntr  24737  icccmplem2  24739  msdcn  24757  cncfmptc  24832  cncfmptid  24833  cncfmpt2f  24835  icoopnst  24863  iocopnst  24864  nmoleub2lem3  25042  nmoleub3  25046  nmhmcn  25047  ipcn  25173  cfilfcls  25201  caucfil  25210  equivcau  25227  caubl  25235  flimcfil  25241  cmssmscld  25277  rrxdstprj1  25336  minveclem3b  25355  minveclem4  25359  mulcncf  25373  ovolicc2lem3  25447  ovolicc2lem4  25448  opnmbllem  25529  vitalilem2  25537  mbfsup  25592  mbfinf  25593  mbfi1fseqlem4  25646  limccnp  25819  limccnp2  25820  dvreslem  25837  dvres2lem  25838  dvidlem  25843  dvcnp2  25848  dvcnp2OLD  25849  dvcn  25850  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  dvcmul  25874  dvcof  25879  dvcnvlem  25907  dvef  25911  rollelem  25920  dvlip2  25927  dvivthlem1  25940  dvivth  25942  lhop2  25947  lhop  25948  dvcnvrelem1  25949  dvcnvrelem2  25950  dvcnvre  25951  ply1rem  26098  fta1blem  26103  plycpn  26224  plyrem  26240  tayl0  26296  dvtaylp  26305  dvntaylp  26306  dvntaylp0  26307  taylthlem1  26308  taylthlem2  26309  taylthlem2OLD  26310  ulmdvlem3  26338  psercn  26363  pserdv  26366  abelth  26378  efabl  26486  efopnlem1  26592  loglesqrt  26698  relogbf  26728  efrlim  26906  efrlimOLD  26907  dchrghm  27194  dchrptlem3  27204  nodenselem5  27627  nosupres  27646  noinfres  27661  sltlpss  27853  precsexlem11  28155  noseq0  28220  noseqp1  28221  noseqrdgfn  28236  noseqrdgsuc  28238  tgbtwntriv2  28465  tgbtwnne  28468  ercgrg  28495  tgidinside  28549  tgbtwnconn1  28553  tglnne  28606  tglnne0  28618  tglnpt2  28619  tglineneq  28622  ncolncol  28624  coltr3  28626  mirln  28654  mirln2  28655  mirconn  28656  krippenlem  28668  footexALT  28696  footexlem1  28697  footexlem2  28698  colperpexlem3  28710  mideulem2  28712  opphllem  28713  oppne3  28721  opphllem1  28725  opphllem2  28726  opphllem4  28728  oppperpex  28731  opphl  28732  hlpasch  28734  hpgerlem  28743  colhp  28748  midbtwn  28757  lmieu  28762  lmiisolem  28774  sacgr  28809  f1otrg  28849  f1otrge  28850  ebtwntg  28960  ecgrtg  28961  eengtrkg  28964  eengtrkge  28965  upgr1eop  29093  usgredg3  29194  uspgr1eop  29225  usgr1eop  29228  vtxdun  29460  vtxdfiun  29461  1loopgruspgr  29479  1loopgrvd2  29482  1hevtxdg1  29485  1egrvtxdg1  29488  1egrvtxdg0  29490  umgr2v2e  29504  wlkres  29647  wlkp1lem4  29653  wlkp1  29658  cyclnumvtx  29778  wwlksm1edg  29859  wwlksnext  29871  wwlksnextproplem3  29889  clwwlkel  30026  1wlkdlem2  30118  trlsegvdeg  30207  eupth2lem3lem1  30208  eupth2lem3lem2  30209  extwwlkfab  30332  numclwlk2lem2f  30357  spansnid  31543  elspansn4  31553  fnpreimac  32653  ccatf1  32930  ccatws1f1olast  32933  swrdrn2  32935  swrdrn3  32936  swrdf1  32937  splfv3  32939  pwrssmgc  32981  wrdpmtrlast  33062  psgnfzto1stlem  33069  cycpmfv1  33082  cycpmfv2  33083  cycpmco2lem2  33096  cycpmco2lem4  33098  cycpmco2lem5  33099  cycpmco2lem6  33100  cycpmco2  33102  cyc3co2  33109  cycpmrn  33112  submarchi  33155  subrdom  33251  fracfld  33274  imaslmod  33318  quslmod  33323  quslmhm  33324  nsgqusf1olem2  33379  lmhmqusker  33382  rhmquskerlem  33390  idlinsubrg  33396  drngidl  33398  rhmpreimaprmidl  33416  qsidomlem2  33418  mxidlprm  33435  opprmxidlabs  33452  qsdrngilem  33459  qsdrngi  33460  qsdrnglem2  33461  idlsrg0g  33471  pidufd  33508  dfufd2lem  33514  fply1  33521  evl1fpws  33527  ressply1evls1  33528  ressply1sub  33533  ply1asclunit  33537  r1plmhm  33570  mplvrpmga  33575  issply  33584  esplympl  33588  drgextlsp  33606  matdim  33628  ply1degltdimlem  33635  lindsunlem  33637  qusdimsum  33641  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  extdg1id  33679  evls1fldgencl  33683  irngss  33700  irngnzply1  33704  extdgfialglem1  33705  extdgfialglem2  33706  minplymindeg  33721  minplyirredlem  33723  irredminply  33729  algextdeglem2  33731  constrconj  33758  constrfiss  33764  1smat1  33817  submat1n  33818  lmatfval  33827  lmatcl  33829  mdetpmtr1  33836  madjusmdetlem4  33843  qtopt1  33848  qtophaus  33849  locfinref  33854  zarcls1  33882  zarclsiin  33884  zarmxt1  33893  zarcmplem  33894  rhmpreimacn  33898  ordtrest2NEWlem  33935  elzrhunit  33990  qqhcn  34004  qqhucn  34005  esumel  34060  esumsplit  34066  sigagenss2  34163  elsx  34207  sxbrsigalem0  34284  dya2icoseg  34290  eulerpartlemb  34381  eulerpartlemgvv  34389  iwrdsplit  34400  sseqfv2  34407  probfinmeasb  34441  dstrvprob  34485  dstfrvel  34487  ballotlemrv  34533  signstfvn  34582  signstfvp  34584  signstfveq0  34590  signsvtp  34596  signsvtn  34597  reprsuc  34628  reprpmtf1o  34639  lpadleft  34696  bnj1006  34972  bnj1018g  34975  bnj1018  34976  bnj1121  34997  bnj1398  35046  bnj1450  35062  bnj1501  35079  revpfxsfxrev  35160  swrdrevpfx  35161  pfxwlk  35168  revwlk  35169  swrdwlk  35171  subfacp1lem5  35228  ptpconn  35277  indispconn  35278  cvxsconn  35287  cvmseu  35320  cvmliftmolem2  35326  cvmliftlem7  35335  cvmliftlem10  35338  cvmliftlem13  35340  cvmlift2lem12  35358  satfv1lem  35406  satffunlem1lem2  35447  satffunlem2lem2  35450  satefvfmla1  35469  mrsubcv  35554  mrsubff  35556  mrsubrn  35557  mrsubccat  35562  elmrsubrn  35564  mrsubco  35565  mrsubvrs  35566  mvhf  35602  msubvrs  35604  mclsax  35613  r1peuqusdeg1  35687  linerflx1  36193  linerflx2  36195  fwddifnval  36207  elhf2  36219  neibastop2lem  36404  weiunpo  36509  weiunso  36510  icoreunrn  37403  relowlssretop  37407  sucneqond  37409  matunitlindflem2  37656  poimirlem4  37663  poimirlem20  37679  poimirlem30  37689  broucube  37693  opnmbllem0  37695  areacirclem2  37748  areacirclem4  37750  blssp  37795  sstotbnd2  37813  totbndbnd  37828  prdstotbnd  37833  cnpwstotbnd  37836  heiborlem9  37858  exidcl  37915  exidresid  37918  grpokerinj  37932  iscringd  38037  erimeq2  38775  prter3  38980  toycom  39071  islfld  39160  lshpsmreu  39207  ldualelvbase  39225  ldualssvscl  39256  lkreqN  39268  lkrlspeqN  39269  erng1lem  41085  erngdvlem4  41089  erng0g  41092  erng1r  41093  erngdvlem4-rN  41097  dva0g  41125  dia1dim2  41160  dia1dimid  41161  dia2dimlem5  41166  dvhelvbasei  41186  dvhvaddass  41195  tendoinvcl  41202  tendolinv  41203  tendorinv  41204  dvhgrp  41205  dvhlveclem  41206  cdlemn4  41296  lcfrlem12N  41652  lcfrlem15  41655  lcdvscl  41703  lcdlssvscl  41704  lcdvsass  41705  lcdvs0N  41714  mapdincl  41759  mapdin  41760  mapdlsmcl  41761  mapdcnvatN  41764  mapdpglem2  41771  mapdpglem12  41781  mapdpglem18  41787  mapdpglem21  41790  mapdpglem22  41791  mapdpglem28  41799  mapdpglem30  41800  hdmaprnlem3N  41948  hdmaprnlem3uN  41949  hdmaprnlem7N  41953  hdmaprnlem8N  41954  hdmaprnlem9N  41955  hdmaprnlem3eN  41956  hdmaprnlem16N  41960  hgmapdcl  41988  hgmapval1  41991  hgmaprnlem4N  41997  hdmapinvlem1  42016  fzadd2d  42070  aks6d1c2lem4  42219  sticksstones1  42238  sticksstones8  42245  sticksstones9  42246  sticksstones10  42247  sticksstones11  42248  sticksstones17  42255  sticksstones18  42256  aks6d1c6lem4  42265  rhmqusspan  42277  aks5lem2  42279  mhmcopsr  42641  evlsbagval  42658  evlsevl  42663  evlvvval  42665  evlvvvallem  42666  selvcllem2  42670  evlselv  42679  mhpind  42686  fltnltalem  42754  wepwsolem  43134  kercvrlsm  43175  dfacbasgrp  43200  onexomgt  43333  onexoegt  43336  onov0suclim  43366  cantnftermord  43412  cantnf2  43417  omcl2  43425  ofoaf  43447  ofoafo  43448  grurankcld  44325  grumnudlem  44377  grumnud  44378  inaex  44389  gruex  44390  dvconstbi  44426  cncmpmax  45128  iooabslt  45598  fmul01lt1lem2  45684  limciccioolb  45720  limcicciooub  45734  limsuppnfdlem  45798  climrescn  45845  climxrrelem  45846  climxrre  45847  liminflimsupxrre  45914  xlimmnfvlem2  45930  xlimpnfvlem2  45934  fsumcncf  45975  ioccncflimc  45982  icocncflimc  45986  cncfiooicclem1  45990  dvbdfbdioolem2  46026  dvnmul  46040  dvnprodlem1  46043  stoweidlem26  46123  stoweidlem34  46131  stoweidlem48  46145  stoweidlem59  46156  dirkercncflem3  46202  fourierdlem32  46236  fourierdlem41  46245  fourierdlem51  46254  fourierdlem63  46266  fourierdlem82  46285  fourierdlem85  46288  fourierdlem93  46296  fourierdlem111  46314  fourierdlem114  46317  etransclem35  46366  hspdifhsp  46713  opnvonmbllem1  46729  ovnovollem1  46753  mbfresmf  46836  smfaddlem1  46860  smfsuplem1  46908  smflimsuplem5  46921  chnerlem2  46980  setsidel  47475  setsnidel  47476  imasetpreimafvbijlemf  47500  prelspr  47585  upgrimpths  48008  gpgprismgr4cycllem9  48202  rngccatidALTV  48371  rhmsubcALTVlem3  48382  funcringcsetcALTV2lem3  48391  funcringcsetcALTV2lem8  48396  ringccatidALTV  48405  funcringcsetclem3ALTV  48414  funcringcsetclem8ALTV  48419  srhmsubcALTVlem1  48422  srhmsubcALTV  48424  lcosslsp  48538  nnolog2flm1  48690  ffvbr  48955  glbprlem  49064  topdlat  49103  catprs  49111  iinfsubc  49158  iinfconstbaslem  49165  imaid  49254  fthcomf  49257  uptr2  49321  natoppf2  49330  natoppfb  49331  swapf2  49374  swapfiso  49385  swapciso  49386  oppc1stflem  49387  cofuswapf2  49395  fuco22natlem  49445  fucoppcffth  49511  oppcthinco  49539  oppcthinendcALT  49541  thinccisod  49554  termco  49581  termchommo  49585  termcid  49586  termcterm  49613  termcterm2  49614  diagciso  49639  diagcic  49640  funcsn  49641  uobeqterm  49646  mndtccatid  49687  grptcmon  49693  grptcepi  49694  2arwcat  49700  lanval2  49727  ranval2  49730  lanup  49741  ranup  49742  lmddu  49767