Theorem eleqtrd 2492

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

Hypotheses

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

Assertion

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

Proof of Theorem eleqtrd

Step	Hyp	Ref	Expression
1		eleqtrd.1	. 2 |- ( ph -> A e. B )
2		eleqtrd.2	. . 3 |- ( ph -> B = C )
3	2	eleq2d 2472	. 2 |- ( ph -> ( A e. B <-> A e. C ) )
4	1, 3	mpbid 210	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1405   e. wcel 1842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-cleq 2394  df-clel 2397

This theorem is referenced by:  eleqtrrd  2493  syl5eleq  2496  syl6eleq  2500  3eltr3d  2504  opth1  4663  0nelop  4679  fviss  5906  tfisi  6675  fnwelem  6898  wfrlem17  7036  omeulem1  7267  oeeulem  7286  oeeui  7287  oaabs2  7330  omabs  7332  ercl  7358  erth  7392  ecelqsdm  7417  ordtypelem6  7981  ordtypelem7  7982  cantnfval  8118  cantnfp1lem3  8130  cantnflem4  8142  cantnfvalOLD  8148  cantnfp1lem3OLD  8156  cantnflem4OLD  8164  r1pwss  8233  rankonidlem  8277  rankxplim3  8330  fseqenlem2  8437  iunfictbso  8526  dfac12lem1  8554  dfac12lem2  8555  fin23lem30  8753  iundom2g  8946  fpwwe2lem6  9042  fpwwe2lem9  9045  lincmb01cmp  11715  fzopth  11773  fzoaddel2  11906  fzosubel2  11910  fzocatel  11914  zpnn0elfzo1  11923  fzoend  11938  peano2fzor  11952  monoord2  12180  sermono  12181  expmulnbnd  12340  bcpasc  12441  swrdcl  12698  revcl  12789  revlen  12790  fsum0diag2  13747  isumsplit  13801  fprodser  13906  sadadd  14324  sadass  14328  smuval2  14339  smumul  14350  vdwapun  14699  vdwlem9  14714  ramub1lem1  14751  prdsbasfn  15083  prdsbasprj  15084  pwsplusgval  15102  pwsmulrval  15103  pwsvscafval  15106  xpsaddlem  15187  xpsvsca  15191  xpsle  15193  mreexmrid  15255  homfeqval  15308  comfval2  15314  comfeq  15317  comfeqval  15319  oppccomfpropd  15338  invco  15382  sectepi  15395  issubc3  15460  funcf2  15479  funciso  15485  fthepi  15539  nat1st2nd  15562  fuciso  15586  homarcl2  15636  coapm  15672  setcmon  15688  setcepi  15689  setcsect  15690  setcinv  15691  setciso  15692  catccatid  15703  resscatc  15706  catciso  15708  catcoppccl  15709  catcfuccl  15710  xpccatid  15779  catcxpccl  15798  xpcpropd  15799  evlfcl  15813  curfpropd  15824  hofcl  15850  yonedalem3  15871  yonffthlem  15873  poslubdg  16101  grpidd  16217  gsumress  16225  ismndd  16265  mndpropd  16268  issubmnd  16270  submnd0  16272  imasmnd  16280  frmdelbas  16343  grpidd2  16409  submmulg  16499  pwsinvg  16504  imasgrp  16508  subginvcl  16532  subgcl  16533  subgsub  16535  subgmulg  16537  quseccl  16579  gaid2  16663  submod  16911  odsubdvds  16913  sylow1lem4  16943  sylow2alem2  16960  lsmdisj2  17022  subgdisj1  17031  pj1id  17039  efgsrel  17074  efgrelexlemb  17090  efgcpbl2  17097  frgpcpbl  17099  frgp0  17100  frgpeccl  17101  frgpadd  17103  frgpup3lem  17117  frgpnabllem1  17199  cycsubgcyg  17225  prdsgsum  17325  prdsgsumOLD  17326  dprdfeq0  17380  dprdfeq0OLD  17387  dmdprdsplitlem  17402  dmdprdsplitlemOLD  17403  dpjidcl  17425  dpjidclOLD  17432  pgpfac1lem3a  17445  pgpfac1lem4  17447  pgpfaclem1  17450  pgpfaclem2  17451  ablfaclem2  17455  ringidss  17543  ringpropd  17548  imasring  17586  qusring2  17587  kerf1hrm  17710  subrg1  17757  subrgmcl  17759  subrgdv  17764  subrgunit  17765  issubdrg  17772  resrhm  17776  lmodprop2d  17890  0lmhm  18004  lmhmpropd  18037  lspfixed  18092  lssacsex  18108  lbsextlem4  18125  quscrng  18206  assapropd  18294  psrelbas  18350  resspsrvsca  18391  subrgpsr  18392  mplcoe1  18445  mplbas2  18452  mplbas2OLD  18453  mplascl  18479  mplmon2cl  18483  mplmon2mul  18484  evlrhm  18512  mpfconst  18517  vr1cl2  18550  ply1lss  18553  ply1subrg  18554  psropprmul  18597  evl1vsd  18698  evl1expd  18699  evl1gsumadd  18712  evl1gsummon  18719  znf1o  18886  psgnghm2  18913  elocv  18995  pjff  19039  frlmlss  19078  frlmsubgval  19092  frlmvscafval  19093  frlmphl  19106  uvcresum  19118  frlmssuvc1  19119  frlmssuvc2  19120  frlmsslsp  19121  frlmup1  19123  matring  19235  matassa  19236  mat1  19239  mattposcl  19245  mavmulass  19341  mdetunilem9  19412  matinv  19469  cpmadugsumlemF  19667  cpmadugsumfi  19668  cpmidgsum2  19670  elcls3  19875  mreclatdemoBAD  19888  neiptopnei  19924  resstps  19979  ordtrest2lem  19995  ordtrest2  19996  pnfnei  20012  mnfnei  20013  iscnp2  20031  iscnp4  20055  cnrest2r  20079  lmcls  20094  lmcld  20095  cnt0  20138  cnhaus  20146  isreg2  20169  conclo  20206  1stccnp  20253  loclly  20278  lly1stc  20287  locfincmp  20317  unisngl  20318  comppfsc  20323  kgencmp2  20337  llycmpkgen2  20341  kgen2ss  20346  kgencn3  20349  pttoponconst  20388  txcls  20395  txbasval  20397  dfac14lem  20408  ptcn  20418  ptrescn  20430  txtube  20431  txcmplem1  20432  txlm  20439  txkgen  20443  xkopjcn  20447  cnmptkp  20471  xkoinjcn  20478  qtopkgen  20501  imastps  20512  isr0  20528  r0cld  20529  pt1hmeo  20597  ptuncnv  20598  ptunhmeo  20599  filintn0  20652  trnei  20683  flimfil  20760  flimopn  20766  fbflim2  20768  cnpflf2  20791  flfcnp  20795  flfcnp2  20798  fclsopn  20805  fcfnei  20826  cnpfcf  20832  alexsublem  20834  ptcmplem3  20844  ptcmplem4  20845  cnextfres  20858  tmdcn2  20878  tmdgsum  20884  tmdgsum2  20885  symgtgp  20890  tgphaus  20905  tgpt1  20906  qustgplem  20909  prdstmdd  20912  prdstgpd  20913  haustsms  20924  tsmscls  20926  tsmsmhm  20938  tsmsadd  20939  tgptsmscls  20942  tsmssplit  20944  restutop  21030  utopreg  21045  ressusp  21058  ucncn  21078  xmetunirn  21130  ressprdsds  21164  xpsdsval  21174  xblss2ps  21194  blbas  21223  mopntopon  21232  isxms2  21241  imasf1oxms  21282  imasf1oms  21283  prdsxmslem2  21322  tmsxpsval  21331  tngngp2  21456  tngngp  21458  tgioo  21591  metdseq0  21648  cncfmpt2f  21708  cncfcnvcn  21715  cnmptre  21717  cnheibor  21745  nmhmcn  21893  cvsdiv  21899  cvsdivcl  21900  cphsubrglem  21914  cphreccllem  21915  iscmet3  22022  relcmpcmet  22045  bcthlem4  22056  rrxds  22115  minveclem4  22137  ivthicc  22160  evthicc  22161  ovolicc2lem4  22221  ovolicc2lem5  22222  iunmbl2  22257  vitalilem3  22309  cncombf  22355  cnmbf  22356  dvres2lem  22604  cpncn  22629  cpnres  22630  dvaddbr  22631  dvmulbr  22632  dvcobr  22639  dvcjbr  22642  dvrec  22648  dvcnvlem  22667  dvlip2  22686  dvivth  22701  lhop2  22706  lhop  22707  dvcnvrelem1  22708  dvcnvrelem2  22709  dvcnvre  22710  ftc1lem6  22732  mdegvscale  22765  mdegvsca  22766  fta1blem  22859  plyaddlem1  22900  plymullem1  22901  coeeulem  22911  tayl0  23047  taylthlem1  23058  taylthlem2  23059  ulmdvlem3  23087  psercnlem2  23109  psercn  23111  efsubm  23228  cxpcn3  23416  loglesqrt  23426  efrlim  23623  ppinprm  23805  chtnprm  23807  dchrptlem1  23918  dchrptlem2  23919  tgbtwnouttr2  24265  tgldim0eq  24273  tgifscgr  24279  ercgrg  24287  tgcgrxfr  24288  motcgrg  24312  tglngne  24318  tgcolg  24322  tgbtwnconn1lem2  24341  tgbtwnconn1lem3  24342  legtri3  24358  legbtwn  24362  ncolne1  24388  tgisline  24390  tglinethru  24399  coltr3  24412  colline  24413  tglowdim2ln  24415  mirinv  24430  miriso  24433  mirauto  24444  miduniq  24445  krippenlem  24450  midexlem  24452  ragperp  24477  footex  24478  perpdragALT  24484  perpdrag  24485  colperpexlem1  24487  colperpexlem3  24489  mideulem2  24491  midex  24494  opphllem1  24502  opphllem3  24504  opphllem4  24505  f1otrg  24578  axlowdimlem16  24664  elntg  24691  eengtrkg  24692  eengtrkge  24693  eupap1  25380  grpoidinv2  25620  grpoinv  25629  ubthlem2  26187  shuni  26618  acunirnmpt  27929  acunirnmpt2  27930  acunirnmpt2f  27931  fpwrelmap  27989  gsummpt2d  28209  rngurd  28217  ordtrest2NEWlem  28343  ordtrest2NEW  28344  lmxrge0  28373  nmmulg  28387  rrhcn  28416  esumadd  28490  esumaddf  28494  esumcocn  28513  measiuns  28651  mbfmco2  28699  dya2iocnrect  28715  omscl  28729  omsf  28730  oms0  28731  sibf0  28768  sibfof  28774  fibp1  28832  ccatmulgnn0dir  28988  bnj1450  29420  bnj1501  29437  indispcon  29518  conpcon  29519  pconpi1  29521  sconpi1  29523  cvmsss2  29558  cvmliftmolem1  29565  cvmliftlem8  29576  cvmliftlem10  29578  cvmliftlem11  29579  cvmlift2lem9  29595  cvmlift2lem12  29598  cvmlift3lem7  29609  mrsubcv  29709  mrsubff  29711  mrsubccat  29717  elmrsubrn  29719  mrsubco  29720  mrsubvrs  29721  linethru  30478  ivthALT  30550  neibastop2  30576  filnetlem4  30596  areacirclem4  31461  fdc  31500  isbnd3  31542  prdsbnd  31551  prdstotbnd  31552  prdsbnd2  31553  rrnequiv  31593  reheibor  31597  iscringd  31658  isfldidl  31727  eqlkr  32097  ldualvsubval  32155  dvalveclem  34025  dia2dimlem5  34068  dia2dimlem9  34072  tendoinvcl  34104  dvhgrp  34107  dvhlveclem  34108  dihpN  34336  dochsnkr2cl  34474  lcfl7lem  34499  lclkr  34533  lclkrs  34539  lcfrvalsnN  34541  lcfrlem4  34545  lcfrlem6  34547  lcfrlem16  34558  lcdvsubval  34618  lcdlkreqN  34622  mapdcl2  34656  mapdincl  34661  mapdlsmcl  34663  mapdpglem3  34675  hdmaprnlem9N  34860  hdmaplkr  34916  hdmapip0  34918  hdmapglem7a  34930  diophin  35047  acongeq  35262  isnumbasgrplem2  35397  proot1mul  35500  iunrelexpuztr  35678  bccbc  36078  suctrALT  36636  monoords  36845  evthiccabs  36878  iooabslt  36881  islptre  36974  limciccioolb  36976  sumnnodd  36985  limcicciooub  36992  lptre2pt  36995  limcresiooub  36997  limcresioolb  36998  lptioo1cn  37001  reclimc  37008  fsumcncf  37029  ioccncflimc  37037  cncfuni  37038  icccncfext  37039  cncficcgt0  37040  icocncflimc  37041  cncfdmsn  37042  cncfiooicclem1  37045  cncfiooicc  37046  cncfioobd  37049  cxpcncf2  37052  fperdvper  37064  dvcosax  37072  dvnmul  37089  dvnprodlem1  37092  dvnprodlem2  37093  itgsubsticclem  37123  stoweidlem26  37157  stoweidlem27  37158  stoweidlem31  37162  stoweidlem34  37165  dirkercncflem2  37235  dirkercncflem3  37236  dirkercncflem4  37237  dirkercncf  37238  fourierdlem16  37254  fourierdlem20  37258  fourierdlem21  37259  fourierdlem22  37260  fourierdlem26  37264  fourierdlem32  37270  fourierdlem33  37271  fourierdlem38  37276  fourierdlem39  37277  fourierdlem46  37284  fourierdlem48  37286  fourierdlem49  37287  fourierdlem53  37291  fourierdlem60  37298  fourierdlem61  37299  fourierdlem69  37307  fourierdlem70  37308  fourierdlem71  37309  fourierdlem73  37311  fourierdlem74  37312  fourierdlem75  37313  fourierdlem76  37314  fourierdlem80  37318  fourierdlem81  37319  fourierdlem82  37320  fourierdlem83  37321  fourierdlem84  37322  fourierdlem85  37323  fourierdlem88  37326  fourierdlem89  37327  fourierdlem91  37329  fourierdlem92  37330  fourierdlem93  37331  fourierdlem100  37338  fourierdlem101  37339  fourierdlem103  37341  fourierdlem104  37342  fourierdlem107  37345  fourierdlem111  37349  fourierdlem112  37350  fourierdlem113  37351  fouriersw  37363  fouriercn  37364  etransclem24  37390  etransclem26  37392  etransclem28  37394  etransclem31  37397  etransclem32  37398  etransclem33  37399  etransclem34  37400  etransclem35  37401  etransclem38  37404  fzoopth  37952  issubmgm2  38088  zlmodzxzel  38436  ply1mulgsum  38482