Theorem eleqtrrd 2843

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731  df-clel 2817

This theorem is referenced by:  3eltr4d  2855  rspc2vd  3887  disjxiun  5075  eldmressnsn  5931  elimdelov  7362  elovmpt3rab1  7520  fnwelem  7956  tfrlem13  8205  tz7.44-2  8222  omordi  8373  oneo  8388  omeulem2  8390  oeordi  8394  oeeui  8409  nnneo  8459  erref  8492  en1uniel  8788  en1unielOLD  8789  omxpenlem  8829  unblem3  9029  dffi3  9151  ordtypelem10  9247  oismo  9260  cantnff  9393  cantnfp1lem3  9399  cantnflem1  9408  cnfcom  9419  r1ordg  9520  r1pwss  9526  rankwflemb  9535  r1elwf  9538  rankidb  9542  rankonidlem  9570  fseqenlem2  9765  dfac12lem1  9883  dfac12lem2  9884  pwsdompw  9944  ackbij2lem3  9981  ackbij2  9983  cfsmolem  10010  hsmexlem4  10169  ttukeylem3  10251  ttukeylem7  10255  iundom2g  10280  fpwwe2lem8  10378  canthwelem  10390  pwfseqlem4  10402  winalim2  10436  r1wunlim  10477  tskmid  10580  fzopth  13275  predfz  13363  fzoss2  13396  fz1fzo0m1  13416  fzo0addel  13422  fzo0addelr  13423  fzosubel3  13429  elfzomin  13440  elfzonlteqm1  13444  fzoend  13459  fzofzp1  13465  fzofzp1b  13466  peano2fzor  13475  zmodfzo  13595  seqf1olem2  13744  bcn2  14014  swrdccat2  14363  pfxccat1  14396  swrdswrd  14399  pfxccatin12  14427  splfv1  14449  revcl  14455  revlen  14456  revccat  14460  revrev  14461  repswpfx  14479  cshwidxmod  14497  revco  14528  limsupgre  15171  summolem2a  15408  fsumm1  15444  fsumcom2  15467  prodmolem2a  15625  fprodm1  15658  fprodcom2  15675  prmreclem4  16601  prmreclem5  16602  vdwapid1  16657  vdwlem5  16667  vdwlem8  16670  vdwnnlem2  16678  ramub1lem1  16708  ramub1lem2  16709  mrieqvlemd  17319  mreexd  17332  mreexexlemd  17334  catcocl  17375  catass  17376  moni  17429  epii  17436  inviso1  17459  episect  17478  invisoinvl  17483  catsubcat  17535  subccocl  17541  fullsubc  17546  funcco  17567  resf2nd  17591  funcres  17592  fthepi  17625  nati  17652  arwhoma  17741  catccatid  17802  resscatc  17805  catcisolem  17806  catcoppccl  17813  catcoppcclOLD  17814  catcfuccl  17815  catcfucclOLD  17816  estrreslem2  17836  funcestrcsetclem3  17840  funcestrcsetclem8  17845  equivestrcsetc  17850  funcsetcestrclem3  17854  funcsetcestrclem8  17860  xpcco  17881  xpcco2  17885  xpccatid  17886  prfcl  17901  catcxpccl  17905  catcxpcclOLD  17906  curf12  17926  curf1cl  17927  curf2  17928  curf2cl  17930  curfcl  17931  uncf2  17936  uncfcurf  17938  diag12  17943  diag2  17944  curf2ndf  17946  hofcl  17958  oppchofcl  17959  oyoncl  17969  yonedalem3a  17973  yonedalem4b  17975  yonedalem22  17977  yonedalem3b  17978  yonedalem3  17979  yonedainv  17980  yonffthlem  17981  latcl2  18135  latlem  18136  latjcom  18146  latmcom  18162  clatlem  18201  clatlubcl2  18203  clatglbcl2  18205  acsfiindd  18252  gsumpropd2lem  18344  mndpropd  18391  imasmnd  18404  frmdmnd  18479  frmdgsum  18482  grpsubpropd2  18662  imasgrp  18672  subg0  18742  0ghm  18829  resghm2  18832  ghmco  18835  pwsdiagghm  18843  psgnunilem1  19082  psgnunilem5  19083  psgnunilem2  19084  psgnunilem3  19085  sylow1lem4  19187  sylow1lem5  19188  efglem  19303  efgtf  19309  efginvrel2  19314  efginvrel1  19315  efgsdmi  19319  efgs1b  19323  efgsres  19325  efgsfo  19326  efgredleme  19330  efgredlemc  19332  efgredlem  19334  efgcpbllemb  19342  frgp0  19347  frgpadd  19350  frgpinv  19351  vrgpf  19355  vrgpinv  19356  frgpuplem  19359  frgpup1  19362  frgpup2  19363  frgpup3lem  19364  frgpnabllem1  19455  frgpnabllem2  19456  gsumval3  19489  dprdfid  19601  dprdsn  19620  dprd2da  19626  dpjidcl  19642  pgpfac1lem2  19659  pgpfaclem3  19667  ablsimpg1gend  19689  ablsimpgprmd  19699  ringpropd  19802  imasring  19839  qusring2  19840  pwsco1rhm  19963  pwsco2rhm  19964  subrgunit  20023  pwsdiagrhm  20039  cntzsdrg  20051  isabvd  20061  lmodprop2d  20166  islssd  20178  prdsvscacl  20211  prdslmodd  20212  islmhm2  20281  lmhmco  20286  lmhmplusg  20287  lmhmvsca  20288  lmhmpropd  20316  lsppreli  20333  lspsnel4  20367  lssacsex  20387  lspsnat  20388  qus1  20487  qusrhm  20489  znf1o  20740  cssmre  20879  dsmmlss  20932  frlmsplit2  20961  frlmbas3  20964  frlmup1  20986  assapropd  21057  psr0cl  21144  psrnegcl  21146  psr1cl  21152  resspsrmul  21167  subrgpsr  21169  mvrf  21174  mplmon  21217  mplcoe1  21219  subrgasclcl  21256  mplind  21259  evlslem1  21273  subrgply1  21385  psrplusgpropd  21388  ply1coe  21448  cply1coe0bi  21452  lply1binomsc  21459  evls1val  21467  evls1rhm  21469  evl1val  21476  evl1rhm  21479  pf1ind  21502  evl1scvarpw  21510  matbas2i  21552  matplusg2  21557  matvsca2  21558  matsubgcell  21564  matvscacell  21566  mpomatmul  21576  mavmulval  21675  mavmulcl  21677  mavmulass  21679  mavmul0  21682  mavmumamul1  21685  m1detdiag  21727  cramerimplem2  21814  mat2pmatmul  21861  mat2pmatlin  21865  monmatcollpw  21909  pmatcollpwfi  21912  mply1topmatcl  21935  pm2mpghm  21946  pm2mpmhmlem2  21949  pm2mp  21955  chpmat1dlem  21965  chpmat1d  21966  chpdmatlem0  21967  chpscmat  21972  chpscmatgsumbin  21974  chpscmatgsummon  21975  chfacfscmulcl  21987  cpmadugsumlemB  22004  cpmadugsumlemC  22005  chcoeffeqlem  22015  cldmreon  22226  neiptopreu  22265  maxlp  22279  ordttopon  22325  ordtrest2lem  22335  cnprcl2  22383  lmcnp  22436  resthauslem  22495  hauscmplem  22538  1stcfb  22577  2ndcctbss  22587  2ndcomap  22590  dis2ndc  22592  loclly  22619  hausllycmp  22626  locfincmp  22658  dissnref  22660  kgeni  22669  kgenidm  22679  ptpjpre2  22712  xkoopn  22721  txopn  22734  ptpjopn  22744  ptcldmpt  22746  ptcls  22748  pthaus  22770  txkgen  22784  xkohaus  22785  xkopt  22787  txconn  22821  imastps  22853  kqid  22860  kqopn  22866  kqcld  22867  isr0  22869  indishmph  22930  pt1hmeo  22938  ptuncnv  22939  ptunhmeo  22940  t0kq  22950  filconn  23015  uzrest  23029  uffixsn  23057  fmfnfmlem2  23087  flimss2  23104  flimss1  23105  flimclslem  23116  flfcnp  23136  fclsfnflim  23159  uffclsflim  23163  fcfelbas  23168  alexsublem  23176  alexsub  23177  cnextcn  23199  cnextfres1  23200  cnextfres  23201  tmdgsum  23227  distgp  23231  indistgp  23232  symgtgp  23238  ghmcnp  23247  qustgpopn  23252  qustgplem  23253  qustgphaus  23255  prdstmdd  23256  prdstgpd  23257  tsmsid  23272  tsmssubm  23275  tsmsmhm  23278  tsmsadd  23279  tsmssplit  23284  utop2nei  23383  utop3cls  23384  neipcfilu  23429  cnextucn  23436  ucnextcn  23437  blpnfctr  23570  lpbl  23640  met2ndci  23659  tmsxps  23673  metcnpi  23681  metcnpi2  23682  metcnpi3  23683  metustid  23691  metustsym  23692  metustexhalf  23693  subgngp  23772  ngptgp  23773  sranlm  23829  nlmvscn  23832  nrginvrcn  23837  lssnlm  23846  nghmcn  23890  iccntr  23965  icccmplem2  23967  msdcn  23985  cncfmptc  24056  cncfmptid  24057  cncfmpt2f  24059  icoopnst  24083  iocopnst  24084  nmoleub2lem3  24259  nmoleub3  24263  nmhmcn  24264  ipcn  24391  cfilfcls  24419  caucfil  24428  equivcau  24445  caubl  24453  flimcfil  24459  cmssmscld  24495  rrxdstprj1  24554  minveclem3b  24573  minveclem4  24577  ovolicc2lem3  24664  ovolicc2lem4  24665  opnmbllem  24746  vitalilem2  24754  mbfsup  24809  mbfinf  24810  mbfi1fseqlem4  24864  limccnp  25036  limccnp2  25037  dvreslem  25054  dvres2lem  25055  dvidlem  25060  dvcnp2  25065  dvcn  25066  dvaddbr  25083  dvmulbr  25084  dvcmul  25089  dvcof  25093  dvcnvlem  25121  dvef  25125  rollelem  25134  dvlip2  25140  dvivthlem1  25153  dvivth  25155  lhop2  25160  lhop  25161  dvcnvrelem1  25162  dvcnvrelem2  25163  dvcnvre  25164  ply1rem  25309  fta1blem  25314  plycpn  25430  plyrem  25446  tayl0  25502  dvtaylp  25510  dvntaylp  25511  dvntaylp0  25512  taylthlem1  25513  taylthlem2  25514  ulmdvlem3  25542  psercn  25566  pserdv  25569  abelth  25581  efabl  25687  efopnlem1  25792  loglesqrt  25892  relogbf  25922  efrlim  26100  dchrghm  26385  dchrptlem3  26395  tgbtwntriv2  26829  tgbtwnne  26832  ercgrg  26859  tgidinside  26913  tgbtwnconn1  26917  tglnne  26970  tglnne0  26982  tglnpt2  26983  tglineneq  26986  ncolncol  26988  coltr3  26990  mirln  27018  mirln2  27019  mirconn  27020  krippenlem  27032  footexALT  27060  footexlem1  27061  footexlem2  27062  colperpexlem3  27074  mideulem2  27076  opphllem  27077  oppne3  27085  opphllem1  27089  opphllem2  27090  opphllem4  27092  oppperpex  27095  opphl  27096  hlpasch  27098  hpgerlem  27107  colhp  27112  midbtwn  27121  lmieu  27126  lmiisolem  27138  sacgr  27173  f1otrg  27213  f1otrge  27214  ebtwntg  27331  ecgrtg  27332  eengtrkg  27335  eengtrkge  27336  upgr1eop  27466  usgredg3  27564  uspgr1eop  27595  usgr1eop  27598  vtxdun  27829  vtxdfiun  27830  1loopgruspgr  27848  1loopgrvd2  27851  1hevtxdg1  27854  1egrvtxdg1  27857  1egrvtxdg0  27859  umgr2v2e  27873  wlkres  28018  wlkp1lem4  28024  wlkp1  28029  wwlksm1edg  28225  wwlksnext  28237  wwlksnextproplem3  28255  clwwlkel  28389  1wlkdlem2  28481  trlsegvdeg  28570  eupth2lem3lem1  28571  eupth2lem3lem2  28572  extwwlkfab  28695  numclwlk2lem2f  28720  spansnid  29904  elspansn4  29914  fnpreimac  30987  ccatf1  31202  swrdrn2  31205  swrdrn3  31206  swrdf1  31207  splfv3  31209  pwrssmgc  31257  psgnfzto1stlem  31346  cycpmfv1  31359  cycpmfv2  31360  cycpmco2lem2  31373  cycpmco2lem4  31375  cycpmco2lem5  31376  cycpmco2lem6  31377  cycpmco2  31379  cyc3co2  31386  cycpmrn  31389  submarchi  31419  imaslmod  31532  quslmod  31533  quslmhm  31534  nsgqusf1olem2  31578  rhmpreimaidl  31582  idlinsubrg  31587  lidlnsg  31600  rhmpreimaprmidl  31606  qsidomlem2  31608  mxidlprm  31619  idlsrg0g  31630  fply1  31646  ply1fermltl  31649  drgextlsp  31660  matdim  31677  lindsunlem  31684  qusdimsum  31688  fedgmullem1  31689  fedgmullem2  31690  fedgmul  31691  extdg1id  31717  1smat1  31733  submat1n  31734  lmatfval  31743  lmatcl  31745  mdetpmtr1  31752  madjusmdetlem4  31759  qtopt1  31764  qtophaus  31765  locfinref  31770  zarcls1  31798  zarclsiin  31800  zarmxt1  31809  zarcmplem  31810  rhmpreimacn  31814  ordtrest2NEWlem  31851  elzrhunit  31908  qqhcn  31920  qqhucn  31921  esumel  31994  esumsplit  32000  sigagenss2  32097  elsx  32141  sxbrsigalem0  32217  dya2icoseg  32223  eulerpartlemb  32314  eulerpartlemgvv  32322  iwrdsplit  32333  sseqfv2  32340  probfinmeasb  32374  dstrvprob  32417  dstfrvel  32419  ballotlemrv  32465  signstfvn  32527  signstfvp  32529  signstfveq0  32535  signsvtp  32541  signsvtn  32542  reprsuc  32574  reprpmtf1o  32585  lpadleft  32642  bnj1006  32919  bnj1018g  32922  bnj1018  32923  bnj1121  32944  bnj1398  32993  bnj1450  33009  bnj1501  33026  revpfxsfxrev  33056  swrdrevpfx  33057  pfxwlk  33064  revwlk  33065  swrdwlk  33067  subfacp1lem5  33125  ptpconn  33174  indispconn  33175  cvxsconn  33184  cvmseu  33217  cvmliftmolem2  33223  cvmliftlem7  33232  cvmliftlem10  33235  cvmliftlem13  33237  cvmlift2lem12  33255  satfv1lem  33303  satffunlem1lem2  33344  satffunlem2lem2  33347  satefvfmla1  33366  mrsubcv  33451  mrsubff  33453  mrsubrn  33454  mrsubccat  33459  elmrsubrn  33461  mrsubco  33462  mrsubvrs  33463  mvhf  33499  msubvrs  33501  mclsax  33510  naddelim  33817  nodenselem5  33870  nosupres  33889  noinfres  33904  sltlpss  34066  linerflx1  34430  linerflx2  34432  fwddifnval  34444  elhf2  34456  neibastop2lem  34528  icoreunrn  35509  relowlssretop  35513  sucneqond  35515  matunitlindflem2  35753  poimirlem4  35760  poimirlem20  35776  poimirlem30  35786  broucube  35790  opnmbllem0  35792  areacirclem2  35845  areacirclem4  35847  blssp  35893  sstotbnd2  35911  totbndbnd  35926  prdstotbnd  35931  cnpwstotbnd  35934  heiborlem9  35956  exidcl  36013  exidresid  36016  grpokerinj  36030  iscringd  36135  erim2  36768  prter3  36875  toycom  36966  islfld  37055  lshpsmreu  37102  ldualelvbase  37120  ldualssvscl  37151  lkreqN  37163  lkrlspeqN  37164  erng1lem  38980  erngdvlem4  38984  erng0g  38987  erng1r  38988  erngdvlem4-rN  38992  dva0g  39020  dia1dim2  39055  dia1dimid  39056  dia2dimlem5  39061  dvhelvbasei  39081  dvhvaddass  39090  tendoinvcl  39097  tendolinv  39098  tendorinv  39099  dvhgrp  39100  dvhlveclem  39101  cdlemn4  39191  lcfrlem12N  39547  lcfrlem15  39550  lcdvscl  39598  lcdlssvscl  39599  lcdvsass  39600  lcdvs0N  39609  mapdincl  39654  mapdin  39655  mapdlsmcl  39656  mapdcnvatN  39659  mapdpglem2  39666  mapdpglem12  39676  mapdpglem18  39682  mapdpglem21  39685  mapdpglem22  39686  mapdpglem28  39694  mapdpglem30  39695  hdmaprnlem3N  39843  hdmaprnlem3uN  39844  hdmaprnlem7N  39848  hdmaprnlem8N  39849  hdmaprnlem9N  39850  hdmaprnlem3eN  39851  hdmaprnlem16N  39855  hgmapdcl  39883  hgmapval1  39886  hgmaprnlem4N  39892  hdmapinvlem1  39911  fzadd2d  39966  sticksstones1  40082  sticksstones8  40089  sticksstones9  40090  sticksstones10  40091  sticksstones11  40092  sticksstones17  40099  sticksstones18  40100  fnsnbt  40188  selvval2lem2  40205  selvval2lem4  40208  evlsbagval  40255  mhpind  40263  mhphf  40265  fltnltalem  40479  wepwsolem  40847  kercvrlsm  40888  dfacbasgrp  40913  imo72b2lem0  41729  grurankcld  41804  grumnudlem  41856  grumnud  41857  inaex  41868  gruex  41869  dvconstbi  41905  cncmpmax  42528  iooabslt  42991  fmul01lt1lem2  43080  limciccioolb  43116  limcicciooub  43132  limsuppnfdlem  43196  climrescn  43243  climxrrelem  43244  climxrre  43245  liminflimsupxrre  43312  xlimmnfvlem2  43328  xlimpnfvlem2  43332  fsumcncf  43373  ioccncflimc  43380  icocncflimc  43384  cncfiooicclem1  43388  dvbdfbdioolem2  43424  dvnmul  43438  stoweidlem26  43521  stoweidlem34  43529  stoweidlem48  43543  stoweidlem59  43554  dirkercncflem3  43600  fourierdlem32  43634  fourierdlem41  43643  fourierdlem51  43652  fourierdlem63  43664  fourierdlem82  43683  fourierdlem85  43686  fourierdlem93  43694  fourierdlem111  43712  fourierdlem114  43715  etransclem35  43764  hspdifhsp  44108  opnvonmbllem1  44124  ovnovollem1  44148  mbfresmf  44226  smfaddlem1  44249  smfsuplem1  44295  smflimsuplem5  44308  fzoopth  44771  setsidel  44780  setsnidel  44781  imasetpreimafvbijlemf  44805  prelspr  44890  rnghmsubcsetclem1  45485  rngccatidALTV  45499  zrinitorngc  45510  zrtermorngc  45511  zrzeroorngc  45512  rhmsubcsetclem1  45531  rhmsubcrngclem1  45537  funcringcsetcALTV2lem3  45548  funcringcsetcALTV2lem8  45553  ringccatidALTV  45562  funcringcsetclem3ALTV  45571  funcringcsetclem8ALTV  45576  irinitoringc  45579  zrtermoringc  45580  zrninitoringc  45581  nzerooringczr  45582  srhmsubclem2  45584  srhmsubc  45586  srhmsubcALTVlem1  45602  srhmsubcALTV  45604  rhmsubcALTVlem3  45616  lcosslsp  45731  nnolog2flm1  45888  glbprlem  46211  topdlat  46242  catprs  46244  mndtccatid  46326  grptcmon  46329  grptcepi  46330