Theorem eleqtrrd 2704

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eleqtrrd.1	|- ( ph -> A e. B )
eleqtrrd.2	|- ( ph -> C = B )

Assertion

Ref	Expression
eleqtrrd	|- ( ph -> A e. C )

Proof of Theorem eleqtrrd

Step	Hyp	Ref	Expression
1		eleqtrrd.1	. 2 |- ( ph -> A e. B )
2		eleqtrrd.2	. . 3 |- ( ph -> C = B )
3	2	eqcomd 2628	. 2 |- ( ph -> B = C )
4	1, 3	eleqtrd 2703	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  3eltr4d  2716  disjxiun  4649  disjxiunOLD  4650  eldmressnsn  5439  elimdelov  6736  elovmpt3rab1  6893  fnwelem  7292  tfrlem13  7486  tz7.44-2  7503  omordi  7646  oneo  7661  omeulem2  7663  oeordi  7667  oeeui  7682  nnneo  7731  erref  7762  en1uniel  8028  omxpenlem  8061  unblem3  8214  dffi3  8337  ordtypelem10  8432  oismo  8445  cantnff  8571  cantnfp1lem3  8577  cantnflem1  8586  cnfcom  8597  r1ordg  8641  r1pwss  8647  rankwflemb  8656  r1elwf  8659  rankidb  8663  rankonidlem  8691  fseqenlem2  8848  dfac12lem1  8965  dfac12lem2  8966  pwsdompw  9026  ackbij2lem3  9063  ackbij2  9065  cfsmolem  9092  isfin4-3  9137  hsmexlem4  9251  ttukeylem3  9333  ttukeylem7  9337  iundom2g  9362  fpwwe2lem9  9460  canthwelem  9472  pwfseqlem4  9484  winalim2  9518  r1wunlim  9559  tskmid  9662  fzopth  12378  predfz  12464  fzoss2  12496  fz1fzo0m1  12515  fzo0addel  12521  fzo0addelr  12522  fzosubel3  12528  elfzomin  12539  elfzonlteqm1  12543  fzoend  12559  fzofzp1  12565  fzofzp1b  12566  peano2fzor  12575  zmodfzo  12693  seqf1olem2  12841  bcn2  13106  swrdccat2  13458  swrdswrd  13460  swrdccatin12  13491  splfv1  13506  revcl  13510  revlen  13511  revccat  13515  revrev  13516  cshwidxmod  13549  revco  13580  limsupgre  14212  summolem2a  14446  fsumm1  14480  fsumcom2  14505  fsumcom2OLD  14506  prodmolem2a  14664  fprodm1  14697  fprodcom2  14714  fprodcom2OLD  14715  prmreclem4  15623  prmreclem5  15624  vdwapid1  15679  vdwlem5  15689  vdwlem8  15692  vdwnnlem2  15700  ramub1lem1  15730  ramub1lem2  15731  mrieqvlemd  16289  mreexd  16302  mreexexlemd  16304  catcocl  16346  catass  16347  moni  16396  epii  16403  inviso1  16426  episect  16445  invisoinvl  16450  catsubcat  16499  subccocl  16505  fullsubc  16510  funcco  16531  resf2nd  16555  funcres  16556  fthepi  16588  nati  16615  arwhoma  16695  catccatid  16752  resscatc  16755  catcisolem  16756  catcoppccl  16758  catcfuccl  16759  estrreslem2  16778  funcestrcsetclem3  16782  funcestrcsetclem8  16787  equivestrcsetc  16792  funcsetcestrclem3  16796  funcsetcestrclem8  16802  xpcco  16823  xpcco2  16827  xpccatid  16828  prfcl  16843  catcxpccl  16847  curf12  16867  curf1cl  16868  curf2  16869  curf2cl  16871  curfcl  16872  uncf2  16877  uncfcurf  16879  diag12  16884  diag2  16885  curf2ndf  16887  hofcl  16899  oppchofcl  16900  oyoncl  16910  yonedalem3a  16914  yonedalem4b  16916  yonedalem22  16918  yonedalem3b  16919  yonedalem3  16920  yonedainv  16921  yonffthlem  16922  latcl2  17048  latlem  17049  latjcom  17059  latmcom  17075  clatlem  17111  clatlubcl2  17113  clatglbcl2  17115  acsfiindd  17177  gsumpropd2lem  17273  mndpropd  17316  imasmnd  17328  frmdmnd  17396  frmdgsum  17399  grpsubpropd2  17521  imasgrp  17531  subg0  17600  0ghm  17674  resghm2  17677  ghmco  17680  pwsdiagghm  17688  psgnunilem1  17913  psgnunilem5  17914  psgnunilem2  17915  psgnunilem3  17916  sylow1lem4  18016  sylow1lem5  18017  efglem  18129  efgtf  18135  efginvrel2  18140  efginvrel1  18141  efgsdmi  18145  efgs1b  18149  efgsres  18151  efgsfo  18152  efgredleme  18156  efgredlemc  18158  efgredlem  18160  efgcpbllemb  18168  frgp0  18173  frgpadd  18176  frgpinv  18177  vrgpf  18181  vrgpinv  18182  frgpuplem  18185  frgpup1  18188  frgpup2  18189  frgpup3lem  18190  frgpnabllem1  18276  frgpnabllem2  18277  gsumval3  18308  dprdfid  18416  dprdsn  18435  dprd2da  18441  dpjidcl  18457  pgpfac1lem2  18474  pgpfaclem3  18482  ringpropd  18582  imasring  18619  qusring2  18620  pwsco1rhm  18738  pwsco2rhm  18739  subrgunit  18798  pwsdiagrhm  18813  isabvd  18820  lmodprop2d  18925  islssd  18936  prdsvscacl  18968  prdslmodd  18969  islmhm2  19038  lmhmco  19043  lmhmplusg  19044  lmhmvsca  19045  lmhmpropd  19073  lsppreli  19090  lspsnel4  19124  lssacsex  19144  lspsnat  19145  qus1  19235  qusrhm  19237  assapropd  19327  psr0cl  19394  psrnegcl  19396  psr1cl  19402  resspsrmul  19417  subrgpsr  19419  mvrf  19424  mplmon  19463  mplcoe1  19465  subrgasclcl  19499  mplind  19502  evlslem1  19515  subrgply1  19603  psrplusgpropd  19606  ply1coe  19666  cply1coe0bi  19670  lply1binomsc  19677  evls1val  19685  evls1rhm  19687  evl1val  19693  evl1rhm  19696  pf1ind  19719  evl1scvarpw  19727  znf1o  19900  cssmre  20037  dsmmlss  20088  frlmsplit2  20112  frlmbas3  20115  frlmup1  20137  matbas2i  20228  matplusg2  20233  matvsca2  20234  matsubgcell  20240  matvscacell  20242  mpt2matmul  20252  mavmulval  20351  mavmulcl  20353  mavmulass  20355  mavmul0  20358  mavmumamul1  20361  m1detdiag  20403  cramerimplem2  20490  mat2pmatmul  20536  mat2pmatlin  20540  monmatcollpw  20584  pmatcollpwfi  20587  mply1topmatcl  20610  pm2mpghm  20621  pm2mpmhmlem2  20624  pm2mp  20630  chpmat1dlem  20640  chpmat1d  20641  chpdmatlem0  20642  chpscmat  20647  chpscmatgsumbin  20649  chpscmatgsummon  20650  chfacfscmulcl  20662  cpmadugsumlemB  20679  cpmadugsumlemC  20680  chcoeffeqlem  20690  cldmreon  20898  neiptopreu  20937  maxlp  20951  ordttopon  20997  ordtrest2lem  21007  cnprcl2  21055  lmcnp  21108  resthauslem  21167  hauscmplem  21209  1stcfb  21248  2ndcctbss  21258  2ndcomap  21261  dis2ndc  21263  loclly  21290  hausllycmp  21297  locfincmp  21329  dissnref  21331  kgeni  21340  kgenidm  21350  ptpjpre2  21383  xkoopn  21392  txopn  21405  ptpjopn  21415  ptcldmpt  21417  ptcls  21419  pthaus  21441  txkgen  21455  xkohaus  21456  xkopt  21458  txconn  21492  imastps  21524  kqid  21531  kqopn  21537  kqcld  21538  isr0  21540  indishmph  21601  pt1hmeo  21609  ptuncnv  21610  ptunhmeo  21611  t0kq  21621  filconn  21687  uzrest  21701  uffixsn  21729  fmfnfmlem2  21759  flimss2  21776  flimss1  21777  flimclslem  21788  flfcnp  21808  fclsfnflim  21831  uffclsflim  21835  fcfelbas  21840  alexsublem  21848  alexsub  21849  cnextcn  21871  cnextfres1  21872  tmdgsum  21899  distgp  21903  indistgp  21904  symgtgp  21905  ghmcnp  21918  qustgpopn  21923  qustgplem  21924  qustgphaus  21926  prdstmdd  21927  prdstgpd  21928  tsmsid  21943  tsmssubm  21946  tsmsmhm  21949  tsmsadd  21950  tsmssplit  21955  utop2nei  22054  utop3cls  22055  neipcfilu  22100  cnextucn  22107  ucnextcn  22108  blpnfctr  22241  lpbl  22308  met2ndci  22327  tmsxps  22341  metcnpi  22349  metcnpi2  22350  metcnpi3  22351  metustid  22359  metustsym  22360  metustexhalf  22361  subgngp  22439  ngptgp  22440  sranlm  22488  nlmvscn  22491  nrginvrcn  22496  lssnlm  22505  nghmcn  22549  iccntr  22624  icccmplem2  22626  msdcn  22644  cncfmptc  22714  cncfmptid  22715  cncfmpt2f  22717  icoopnst  22738  iocopnst  22739  nmoleub2lem3  22915  nmoleub3  22919  nmhmcn  22920  ipcn  23045  cfilfcls  23072  caucfil  23081  equivcau  23098  caubl  23106  flimcfil  23112  rrxdstprj1  23192  minveclem3b  23199  minveclem4  23203  ovolicc2lem3  23287  ovolicc2lem4  23288  opnmbllem  23369  vitalilem2  23378  mbfsup  23431  mbfinf  23432  mbfi1fseqlem4  23485  limccnp  23655  limccnp2  23656  dvreslem  23673  dvres2lem  23674  dvidlem  23679  dvcnp2  23683  dvcn  23684  dvaddbr  23701  dvmulbr  23702  dvcmul  23707  dvcof  23711  dvcnvlem  23739  dvef  23743  rollelem  23752  dvlip2  23758  dvivthlem1  23771  dvivth  23773  lhop2  23778  lhop  23779  dvcnvrelem1  23780  dvcnvrelem2  23781  dvcnvre  23782  ply1rem  23923  fta1blem  23928  plycpn  24044  plyrem  24060  tayl0  24116  dvtaylp  24124  dvntaylp  24125  dvntaylp0  24126  taylthlem1  24127  taylthlem2  24128  ulmdvlem3  24156  psercn  24180  pserdv  24183  abelth  24195  efabl  24296  efopnlem1  24402  loglesqrt  24499  relogbf  24529  efrlim  24696  dchrghm  24981  dchrptlem3  24991  tgbtwntriv2  25382  tgbtwnne  25385  ercgrg  25412  tgidinside  25466  tgbtwnconn1  25470  tglnne  25523  tglnne0  25535  tglnpt2  25536  tglineneq  25539  ncolncol  25541  coltr3  25543  mirln  25571  mirln2  25572  mirconn  25573  krippenlem  25585  footex  25613  colperpexlem3  25624  mideulem2  25626  opphllem  25627  oppne3  25635  opphllem1  25639  opphllem2  25640  opphllem4  25642  oppperpex  25645  opphl  25646  hlpasch  25648  hpgerlem  25657  colhp  25662  midbtwn  25671  lmieu  25676  lmiisolem  25688  sacgr  25722  f1otrg  25751  f1otrge  25752  ebtwntg  25862  ecgrtg  25863  eengtrkg  25865  eengtrkge  25866  upgr1eop  26010  usgredg3  26108  uspgr1eop  26139  usgr1eop  26142  vtxdun  26377  vtxdfiun  26378  1loopgruspgr  26396  1loopgrvd2  26399  1hevtxdg1  26402  1egrvtxdg1  26405  1egrvtxdg0  26407  umgr2v2e  26421  wlkres  26567  wlkp1lem4  26573  wlkp1  26578  wwlksm1edg  26767  wwlksnext  26788  wwlksnextproplem1  26804  wwlksnextproplem3  26806  clwwlksel  26914  1wlkdlem2  26998  trlsegvdeg  27087  eupth2lem3lem1  27088  eupth2lem3lem2  27089  rspc2vd  27129  extwwlkfablem2  27210  extwwlkfab  27223  numclwlk1lem2foa  27224  numclwlk2lem2f  27236  spansnid  28422  elspansn4  28432  submarchi  29740  psgnfzto1stlem  29850  1smat1  29870  submat1n  29871  lmatfval  29880  lmatcl  29882  mdetpmtr1  29889  madjusmdetlem4  29896  qtopt1  29902  qtophaus  29903  locfinref  29908  ordtrest2NEWlem  29968  elzrhunit  30023  qqhcn  30035  qqhucn  30036  esumel  30109  esumsplit  30115  sigagenss2  30213  elsx  30257  sxbrsigalem0  30333  dya2icoseg  30339  eulerpartlemb  30430  eulerpartlemgvv  30438  iwrdsplit  30449  sseqfv2  30456  probfinmeasb  30491  dstrvprob  30533  dstfrvel  30535  ballotlemrv  30581  signstfvn  30646  signstfvp  30648  signstfveq0  30654  signsvtp  30660  signsvtn  30661  reprsuc  30693  reprpmtf1o  30704  bnj1006  31029  bnj1018  31032  bnj1121  31053  bnj1398  31102  bnj1450  31118  bnj1501  31135  subfacp1lem5  31166  ptpconn  31215  indispconn  31216  cvxsconn  31225  cvmseu  31258  cvmliftmolem2  31264  cvmliftlem7  31273  cvmliftlem10  31276  cvmliftlem13  31278  cvmlift2lem12  31296  mrsubcv  31407  mrsubff  31409  mrsubrn  31410  mrsubccat  31415  elmrsubrn  31417  mrsubco  31418  mrsubvrs  31419  mvhf  31455  msubvrs  31457  mclsax  31466  nodenselem5  31838  nosupres  31853  linerflx1  32256  linerflx2  32258  fwddifnval  32270  elhf2  32282  neibastop2lem  32355  icoreunrn  33207  relowlssretop  33211  sucneqond  33213  matunitlindflem2  33406  poimirlem4  33413  poimirlem20  33429  poimirlem30  33439  broucube  33443  opnmbllem0  33445  areacirclem2  33501  areacirclem4  33503  blssp  33552  sstotbnd2  33573  totbndbnd  33588  prdstotbnd  33593  cnpwstotbnd  33596  heiborlem9  33618  exidcl  33675  exidresid  33678  grpokerinj  33692  iscringd  33797  prter3  34167  toycom  34260  islfld  34349  lshpsmreu  34396  ldualelvbase  34414  ldualssvscl  34445  lkreqN  34457  lkrlspeqN  34458  erng1lem  36275  erngdvlem4  36279  erng0g  36282  erng1r  36283  erngdvlem4-rN  36287  dva0g  36316  dia1dim2  36351  dia1dimid  36352  dia2dimlem5  36357  dvhelvbasei  36377  dvhvaddass  36386  tendoinvcl  36393  tendolinv  36394  tendorinv  36395  dvhgrp  36396  dvhlveclem  36397  cdlemn4  36487  lcfrlem12N  36843  lcfrlem15  36846  lcdvscl  36894  lcdlssvscl  36895  lcdvsass  36896  lcdvs0N  36905  mapdincl  36950  mapdin  36951  mapdlsmcl  36952  mapdcnvatN  36955  mapdpglem2  36962  mapdpglem12  36972  mapdpglem18  36978  mapdpglem21  36981  mapdpglem22  36982  mapdpglem28  36990  mapdpglem30  36991  hdmaprnlem3N  37142  hdmaprnlem3uN  37143  hdmaprnlem7N  37147  hdmaprnlem8N  37148  hdmaprnlem9N  37149  hdmaprnlem3eN  37150  hdmaprnlem16N  37154  hgmapdcl  37182  hgmapval1  37185  hgmaprnlem4N  37191  hdmapinvlem1  37210  wepwsolem  37612  kercvrlsm  37653  dfacbasgrp  37678  cntzsdrg  37772  imo72b2lem0  38465  dvconstbi  38533  cncmpmax  39191  iooabslt  39721  fmul01lt1lem2  39817  limciccioolb  39853  limcicciooub  39869  limsuppnfdlem  39933  climrescn  39980  climxrrelem  39981  climxrre  39982  xlimmnfvlem2  40059  xlimpnfvlem2  40063  fsumcncf  40091  ioccncflimc  40098  icocncflimc  40102  cncfiooicclem1  40106  dvbdfbdioolem2  40144  dvnmul  40158  stoweidlem26  40243  stoweidlem34  40251  stoweidlem48  40265  stoweidlem59  40276  dirkercncflem3  40322  fourierdlem32  40356  fourierdlem41  40365  fourierdlem51  40374  fourierdlem63  40386  fourierdlem82  40405  fourierdlem85  40408  fourierdlem93  40416  fourierdlem111  40434  fourierdlem114  40437  etransclem35  40486  hspdifhsp  40830  opnvonmbllem1  40846  ovnovollem1  40870  mbfresmf  40948  smfaddlem1  40971  smfsuplem1  41017  smflimsuplem5  41030  fzoopth  41337  setsidel  41346  setsnidel  41347  pfxccat1  41410  pfxccatin12  41425  repswpfx  41436  prelspr  41736  rnghmsubcsetclem1  41975  rngccatidALTV  41989  zrinitorngc  42000  zrtermorngc  42001  zrzeroorngc  42002  rhmsubcsetclem1  42021  rhmsubcrngclem1  42027  funcringcsetcALTV2lem3  42038  funcringcsetcALTV2lem8  42043  ringccatidALTV  42052  funcringcsetclem3ALTV  42061  funcringcsetclem8ALTV  42066  irinitoringc  42069  zrtermoringc  42070  zrninitoringc  42071  nzerooringczr  42072  srhmsubclem2  42074  srhmsubc  42076  srhmsubcALTVlem1  42092  srhmsubcALTV  42094  rhmsubcALTVlem3  42106  lcosslsp  42227  nnolog2flm1  42384