Theorem eleqtrrd 2837

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  3eltr4d  2849  rspc2vd  3945  disjxiun  5146  eldmressnsn  6025  elimdelov  7505  elovmpt3rab1  7666  fnwelem  8117  tfrlem13  8390  tz7.44-2  8407  omordi  8566  oneo  8581  omeulem2  8583  oeordi  8587  oeeui  8602  nnneo  8654  naddelim  8685  erref  8723  en1uniel  9028  en1unielOLD  9029  omxpenlem  9073  unblem3  9297  dffi3  9426  ordtypelem10  9522  oismo  9535  cantnff  9669  cantnfp1lem3  9675  cantnflem1  9684  cnfcom  9695  r1ordg  9773  r1pwss  9779  rankwflemb  9788  r1elwf  9791  rankidb  9795  rankonidlem  9823  fseqenlem2  10020  dfac12lem1  10138  dfac12lem2  10139  pwsdompw  10199  ackbij2lem3  10236  ackbij2  10238  cfsmolem  10265  hsmexlem4  10424  ttukeylem3  10506  ttukeylem7  10510  iundom2g  10535  fpwwe2lem8  10633  canthwelem  10645  pwfseqlem4  10657  winalim2  10691  r1wunlim  10732  tskmid  10835  fzopth  13538  predfz  13626  fzoss2  13660  fz1fzo0m1  13680  fzo0addel  13686  fzo0addelr  13687  fzosubel3  13693  elfzomin  13704  elfzonlteqm1  13708  fzoend  13723  fzofzp1  13729  fzofzp1b  13730  peano2fzor  13739  zmodfzo  13859  seqf1olem2  14008  bcn2  14279  swrdccat2  14619  pfxccat1  14652  swrdswrd  14655  pfxccatin12  14683  splfv1  14705  revcl  14711  revlen  14712  revccat  14716  revrev  14717  repswpfx  14735  cshwidxmod  14753  revco  14785  limsupgre  15425  summolem2a  15661  fsumm1  15697  fsumcom2  15720  prodmolem2a  15878  fprodm1  15911  fprodcom2  15928  prmreclem4  16852  prmreclem5  16853  vdwapid1  16908  vdwlem5  16918  vdwlem8  16921  vdwnnlem2  16929  ramub1lem1  16959  ramub1lem2  16960  mrieqvlemd  17573  mreexd  17586  mreexexlemd  17588  catcocl  17629  catass  17630  moni  17683  epii  17690  inviso1  17713  episect  17732  invisoinvl  17737  catsubcat  17789  subccocl  17795  fullsubc  17800  funcco  17821  resf2nd  17845  funcres  17846  fthepi  17879  nati  17906  arwhoma  17995  catccatid  18056  resscatc  18059  catcisolem  18060  catcoppccl  18067  catcoppcclOLD  18068  catcfuccl  18069  catcfucclOLD  18070  estrreslem2  18090  funcestrcsetclem3  18094  funcestrcsetclem8  18099  equivestrcsetc  18104  funcsetcestrclem3  18108  funcsetcestrclem8  18114  xpcco  18135  xpcco2  18139  xpccatid  18140  prfcl  18155  catcxpccl  18159  catcxpcclOLD  18160  curf12  18180  curf1cl  18181  curf2  18182  curf2cl  18184  curfcl  18185  uncf2  18190  uncfcurf  18192  diag12  18197  diag2  18198  curf2ndf  18200  hofcl  18212  oppchofcl  18213  oyoncl  18223  yonedalem3a  18227  yonedalem4b  18229  yonedalem22  18231  yonedalem3b  18232  yonedalem3  18233  yonedainv  18234  yonffthlem  18235  latcl2  18389  latlem  18390  latjcom  18400  latmcom  18416  clatlem  18455  clatlubcl2  18457  clatglbcl2  18459  acsfiindd  18506  gsumpropd2lem  18598  sgrppropd  18622  mndpropd  18650  imasmnd  18663  frmdmnd  18740  frmdgsum  18743  grpsubpropd2  18929  imasgrp  18939  subg0  19012  0ghm  19106  resghm2  19109  ghmco  19112  pwsdiagghm  19120  psgnunilem1  19361  psgnunilem5  19362  psgnunilem2  19363  psgnunilem3  19364  sylow1lem4  19469  sylow1lem5  19470  efglem  19584  efgtf  19590  efginvrel2  19595  efginvrel1  19596  efgsdmi  19600  efgs1b  19604  efgsres  19606  efgsfo  19607  efgredleme  19611  efgredlemc  19613  efgredlem  19615  efgcpbllemb  19623  frgp0  19628  frgpadd  19631  frgpinv  19632  vrgpf  19636  vrgpinv  19637  frgpuplem  19640  frgpup1  19643  frgpup2  19644  frgpup3lem  19645  frgpnabllem1  19741  frgpnabllem2  19742  gsumval3  19775  dprdfid  19887  dprdsn  19906  dprd2da  19912  dpjidcl  19928  pgpfac1lem2  19945  pgpfaclem3  19953  ablsimpg1gend  19975  ablsimpgprmd  19985  ringpropd  20102  imasring  20143  qusring2  20147  pwsco1rhm  20277  pwsco2rhm  20278  lringuplu  20314  subrgunit  20337  pwsdiagrhm  20354  cntzsdrg  20418  isabvd  20428  lmodprop2d  20534  islssd  20546  prdsvscacl  20579  prdslmodd  20580  islmhm2  20649  lmhmco  20654  lmhmplusg  20655  lmhmvsca  20656  lmhmpropd  20684  lsppreli  20701  lspsnel4  20737  lssacsex  20757  lspsnat  20758  qus1  20872  qusrhm  20874  znf1o  21107  cssmre  21246  dsmmlss  21299  frlmsplit2  21328  frlmbas3  21331  frlmup1  21353  assapropd  21426  psr0cl  21513  psrnegcl  21515  psr1cl  21522  resspsrmul  21537  subrgpsr  21539  mvrf  21544  mplmon  21590  mplcoe1  21592  subrgasclcl  21628  mplind  21631  evlslem1  21645  subrgply1  21755  psrplusgpropd  21758  ply1coe  21820  cply1coe0bi  21824  lply1binomsc  21831  evls1val  21839  evls1rhm  21841  evl1val  21848  evl1rhm  21851  pf1ind  21874  evl1scvarpw  21882  matbas2i  21924  matplusg2  21929  matvsca2  21930  matsubgcell  21936  matvscacell  21938  mpomatmul  21948  mavmulval  22047  mavmulcl  22049  mavmulass  22051  mavmul0  22054  mavmumamul1  22057  m1detdiag  22099  cramerimplem2  22186  mat2pmatmul  22233  mat2pmatlin  22237  monmatcollpw  22281  pmatcollpwfi  22284  mply1topmatcl  22307  pm2mpghm  22318  pm2mpmhmlem2  22321  pm2mp  22327  chpmat1dlem  22337  chpmat1d  22338  chpdmatlem0  22339  chpscmat  22344  chpscmatgsumbin  22346  chpscmatgsummon  22347  chfacfscmulcl  22359  cpmadugsumlemB  22376  cpmadugsumlemC  22377  chcoeffeqlem  22387  cldmreon  22598  neiptopreu  22637  maxlp  22651  ordttopon  22697  ordtrest2lem  22707  cnprcl2  22755  lmcnp  22808  resthauslem  22867  hauscmplem  22910  1stcfb  22949  2ndcctbss  22959  2ndcomap  22962  dis2ndc  22964  loclly  22991  hausllycmp  22998  locfincmp  23030  dissnref  23032  kgeni  23041  kgenidm  23051  ptpjpre2  23084  xkoopn  23093  txopn  23106  ptpjopn  23116  ptcldmpt  23118  ptcls  23120  pthaus  23142  txkgen  23156  xkohaus  23157  xkopt  23159  txconn  23193  imastps  23225  kqid  23232  kqopn  23238  kqcld  23239  isr0  23241  indishmph  23302  pt1hmeo  23310  ptuncnv  23311  ptunhmeo  23312  t0kq  23322  filconn  23387  uzrest  23401  uffixsn  23429  fmfnfmlem2  23459  flimss2  23476  flimss1  23477  flimclslem  23488  flfcnp  23508  fclsfnflim  23531  uffclsflim  23535  fcfelbas  23540  alexsublem  23548  alexsub  23549  cnextcn  23571  cnextfres1  23572  cnextfres  23573  tmdgsum  23599  distgp  23603  indistgp  23604  symgtgp  23610  ghmcnp  23619  qustgpopn  23624  qustgplem  23625  qustgphaus  23627  prdstmdd  23628  prdstgpd  23629  tsmsid  23644  tsmssubm  23647  tsmsmhm  23650  tsmsadd  23651  tsmssplit  23656  utop2nei  23755  utop3cls  23756  neipcfilu  23801  cnextucn  23808  ucnextcn  23809  blpnfctr  23942  lpbl  24012  met2ndci  24031  tmsxps  24045  metcnpi  24053  metcnpi2  24054  metcnpi3  24055  metustid  24063  metustsym  24064  metustexhalf  24065  subgngp  24144  ngptgp  24145  sranlm  24201  nlmvscn  24204  nrginvrcn  24209  lssnlm  24218  nghmcn  24262  iccntr  24337  icccmplem2  24339  msdcn  24357  cncfmptc  24428  cncfmptid  24429  cncfmpt2f  24431  icoopnst  24455  iocopnst  24456  nmoleub2lem3  24631  nmoleub3  24635  nmhmcn  24636  ipcn  24763  cfilfcls  24791  caucfil  24800  equivcau  24817  caubl  24825  flimcfil  24831  cmssmscld  24867  rrxdstprj1  24926  minveclem3b  24945  minveclem4  24949  ovolicc2lem3  25036  ovolicc2lem4  25037  opnmbllem  25118  vitalilem2  25126  mbfsup  25181  mbfinf  25182  mbfi1fseqlem4  25236  limccnp  25408  limccnp2  25409  dvreslem  25426  dvres2lem  25427  dvidlem  25432  dvcnp2  25437  dvcn  25438  dvaddbr  25455  dvmulbr  25456  dvcmul  25461  dvcof  25465  dvcnvlem  25493  dvef  25497  rollelem  25506  dvlip2  25512  dvivthlem1  25525  dvivth  25527  lhop2  25532  lhop  25533  dvcnvrelem1  25534  dvcnvrelem2  25535  dvcnvre  25536  ply1rem  25681  fta1blem  25686  plycpn  25802  plyrem  25818  tayl0  25874  dvtaylp  25882  dvntaylp  25883  dvntaylp0  25884  taylthlem1  25885  taylthlem2  25886  ulmdvlem3  25914  psercn  25938  pserdv  25941  abelth  25953  efabl  26059  efopnlem1  26164  loglesqrt  26266  relogbf  26296  efrlim  26474  dchrghm  26759  dchrptlem3  26769  nodenselem5  27191  nosupres  27210  noinfres  27225  sltlpss  27401  precsexlem11  27663  tgbtwntriv2  27738  tgbtwnne  27741  ercgrg  27768  tgidinside  27822  tgbtwnconn1  27826  tglnne  27879  tglnne0  27891  tglnpt2  27892  tglineneq  27895  ncolncol  27897  coltr3  27899  mirln  27927  mirln2  27928  mirconn  27929  krippenlem  27941  footexALT  27969  footexlem1  27970  footexlem2  27971  colperpexlem3  27983  mideulem2  27985  opphllem  27986  oppne3  27994  opphllem1  27998  opphllem2  27999  opphllem4  28001  oppperpex  28004  opphl  28005  hlpasch  28007  hpgerlem  28016  colhp  28021  midbtwn  28030  lmieu  28035  lmiisolem  28047  sacgr  28082  f1otrg  28122  f1otrge  28123  ebtwntg  28240  ecgrtg  28241  eengtrkg  28244  eengtrkge  28245  upgr1eop  28375  usgredg3  28473  uspgr1eop  28504  usgr1eop  28507  vtxdun  28738  vtxdfiun  28739  1loopgruspgr  28757  1loopgrvd2  28760  1hevtxdg1  28763  1egrvtxdg1  28766  1egrvtxdg0  28768  umgr2v2e  28782  wlkres  28927  wlkp1lem4  28933  wlkp1  28938  wwlksm1edg  29135  wwlksnext  29147  wwlksnextproplem3  29165  clwwlkel  29299  1wlkdlem2  29391  trlsegvdeg  29480  eupth2lem3lem1  29481  eupth2lem3lem2  29482  extwwlkfab  29605  numclwlk2lem2f  29630  spansnid  30816  elspansn4  30826  fnpreimac  31896  ccatf1  32115  swrdrn2  32118  swrdrn3  32119  swrdf1  32120  splfv3  32122  pwrssmgc  32170  psgnfzto1stlem  32259  cycpmfv1  32272  cycpmfv2  32273  cycpmco2lem2  32286  cycpmco2lem4  32288  cycpmco2lem5  32289  cycpmco2lem6  32290  cycpmco2  32292  cyc3co2  32299  cycpmrn  32302  submarchi  32332  imaslmod  32468  quslmod  32469  quslmhm  32470  nsgqusf1olem2  32525  ghmquskerlem2  32530  ghmquskerlem3  32531  ghmqusker  32532  lmhmqusker  32534  rhmpreimaidl  32537  rhmquskerlem  32543  idlinsubrg  32549  drngidl  32551  lidlnsg  32564  rhmpreimaprmidl  32570  qsidomlem2  32572  mxidlprm  32586  opprmxidlabs  32601  qsdrngilem  32608  qsdrngi  32609  qsdrnglem2  32610  idlsrg0g  32620  fply1  32637  evls1fpws  32646  ply1asclunit  32654  ressply1sub  32659  ply1fermltlchr  32662  drgextlsp  32681  matdim  32700  ply1degltdimlem  32707  lindsunlem  32709  qusdimsum  32713  fedgmullem1  32714  fedgmullem2  32715  fedgmul  32716  extdg1id  32742  irngss  32751  irngnzply1  32755  minplyirredlem  32769  algextdeglem1  32772  1smat1  32784  submat1n  32785  lmatfval  32794  lmatcl  32796  mdetpmtr1  32803  madjusmdetlem4  32810  qtopt1  32815  qtophaus  32816  locfinref  32821  zarcls1  32849  zarclsiin  32851  zarmxt1  32860  zarcmplem  32861  rhmpreimacn  32865  ordtrest2NEWlem  32902  elzrhunit  32959  qqhcn  32971  qqhucn  32972  esumel  33045  esumsplit  33051  sigagenss2  33148  elsx  33192  sxbrsigalem0  33270  dya2icoseg  33276  eulerpartlemb  33367  eulerpartlemgvv  33375  iwrdsplit  33386  sseqfv2  33393  probfinmeasb  33427  dstrvprob  33470  dstfrvel  33472  ballotlemrv  33518  signstfvn  33580  signstfvp  33582  signstfveq0  33588  signsvtp  33594  signsvtn  33595  reprsuc  33627  reprpmtf1o  33638  lpadleft  33695  bnj1006  33971  bnj1018g  33974  bnj1018  33975  bnj1121  33996  bnj1398  34045  bnj1450  34061  bnj1501  34078  revpfxsfxrev  34106  swrdrevpfx  34107  pfxwlk  34114  revwlk  34115  swrdwlk  34117  subfacp1lem5  34175  ptpconn  34224  indispconn  34225  cvxsconn  34234  cvmseu  34267  cvmliftmolem2  34273  cvmliftlem7  34282  cvmliftlem10  34285  cvmliftlem13  34287  cvmlift2lem12  34305  satfv1lem  34353  satffunlem1lem2  34394  satffunlem2lem2  34397  satefvfmla1  34416  mrsubcv  34501  mrsubff  34503  mrsubrn  34504  mrsubccat  34509  elmrsubrn  34511  mrsubco  34512  mrsubvrs  34513  mvhf  34549  msubvrs  34551  mclsax  34560  linerflx1  35121  linerflx2  35123  fwddifnval  35135  elhf2  35147  gg-mulcncf  35173  gg-dvcnp2  35174  gg-dvmulbr  35175  neibastop2lem  35245  icoreunrn  36240  relowlssretop  36244  sucneqond  36246  matunitlindflem2  36485  poimirlem4  36492  poimirlem20  36508  poimirlem30  36518  broucube  36522  opnmbllem0  36524  areacirclem2  36577  areacirclem4  36579  blssp  36624  sstotbnd2  36642  totbndbnd  36657  prdstotbnd  36662  cnpwstotbnd  36665  heiborlem9  36687  exidcl  36744  exidresid  36747  grpokerinj  36761  iscringd  36866  erimeq2  37548  prter3  37752  toycom  37843  islfld  37932  lshpsmreu  37979  ldualelvbase  37997  ldualssvscl  38028  lkreqN  38040  lkrlspeqN  38041  erng1lem  39858  erngdvlem4  39862  erng0g  39865  erng1r  39866  erngdvlem4-rN  39870  dva0g  39898  dia1dim2  39933  dia1dimid  39934  dia2dimlem5  39939  dvhelvbasei  39959  dvhvaddass  39968  tendoinvcl  39975  tendolinv  39976  tendorinv  39977  dvhgrp  39978  dvhlveclem  39979  cdlemn4  40069  lcfrlem12N  40425  lcfrlem15  40428  lcdvscl  40476  lcdlssvscl  40477  lcdvsass  40478  lcdvs0N  40487  mapdincl  40532  mapdin  40533  mapdlsmcl  40534  mapdcnvatN  40537  mapdpglem2  40544  mapdpglem12  40554  mapdpglem18  40560  mapdpglem21  40563  mapdpglem22  40564  mapdpglem28  40572  mapdpglem30  40573  hdmaprnlem3N  40721  hdmaprnlem3uN  40722  hdmaprnlem7N  40726  hdmaprnlem8N  40727  hdmaprnlem9N  40728  hdmaprnlem3eN  40729  hdmaprnlem16N  40733  hgmapdcl  40761  hgmapval1  40764  hgmaprnlem4N  40770  hdmapinvlem1  40789  fzadd2d  40843  sticksstones1  40962  sticksstones8  40969  sticksstones9  40970  sticksstones10  40971  sticksstones11  40972  sticksstones17  40979  sticksstones18  40980  fnsnbt  41051  mhmcompl  41120  evlsbagval  41138  evlsevl  41143  evlvvval  41145  evlvvvallem  41146  selvcllem2  41150  evlselv  41159  mhpind  41166  fltnltalem  41404  wepwsolem  41784  kercvrlsm  41825  dfacbasgrp  41850  onexomgt  41990  onexoegt  41993  onov0suclim  42024  cantnftermord  42070  cantnf2  42075  omcl2  42083  ofoaf  42105  ofoafo  42106  imo72b2lem0  42917  grurankcld  42992  grumnudlem  43044  grumnud  43045  inaex  43056  gruex  43057  dvconstbi  43093  cncmpmax  43716  iooabslt  44212  fmul01lt1lem2  44301  limciccioolb  44337  limcicciooub  44353  limsuppnfdlem  44417  climrescn  44464  climxrrelem  44465  climxrre  44466  liminflimsupxrre  44533  xlimmnfvlem2  44549  xlimpnfvlem2  44553  fsumcncf  44594  ioccncflimc  44601  icocncflimc  44605  cncfiooicclem1  44609  dvbdfbdioolem2  44645  dvnmul  44659  stoweidlem26  44742  stoweidlem34  44750  stoweidlem48  44764  stoweidlem59  44775  dirkercncflem3  44821  fourierdlem32  44855  fourierdlem41  44864  fourierdlem51  44873  fourierdlem63  44885  fourierdlem82  44904  fourierdlem85  44907  fourierdlem93  44915  fourierdlem111  44933  fourierdlem114  44936  etransclem35  44985  hspdifhsp  45332  opnvonmbllem1  45348  ovnovollem1  45372  mbfresmf  45455  smfaddlem1  45479  smfsuplem1  45527  smflimsuplem5  45540  fzoopth  46035  setsidel  46044  setsnidel  46045  imasetpreimafvbijlemf  46069  prelspr  46154  rngpropd  46673  imasrng  46678  qus2idrng  46767  rngqiprngghmlem1  46772  rngqiprngfulem1  46796  rnghmsubcsetclem1  46873  rngccatidALTV  46887  zrinitorngc  46898  zrtermorngc  46899  zrzeroorngc  46900  rhmsubcsetclem1  46919  rhmsubcrngclem1  46925  funcringcsetcALTV2lem3  46936  funcringcsetcALTV2lem8  46941  ringccatidALTV  46950  funcringcsetclem3ALTV  46959  funcringcsetclem8ALTV  46964  irinitoringc  46967  zrtermoringc  46968  zrninitoringc  46969  nzerooringczr  46970  srhmsubclem2  46972  srhmsubc  46974  srhmsubcALTVlem1  46990  srhmsubcALTV  46992  rhmsubcALTVlem3  47004  lcosslsp  47119  nnolog2flm1  47276  glbprlem  47598  topdlat  47629  catprs  47631  mndtccatid  47713  grptcmon  47716  grptcepi  47717