Theorem eleqtrd 2510

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 2490	. 2 |- ( ph -> ( A e. B <-> A e. C ) )
4	1, 3	mpbid 213	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1437   e. wcel 1867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-cleq 2412  df-clel 2415

This theorem is referenced by:  eleqtrrd  2511  syl5eleq  2514  syl6eleq  2518  3eltr3d  2522  opth1  4687  0nelop  4703  fviss  5931  tfisi  6691  fnwelem  6914  wfrlem17  7052  omeulem1  7283  oeeulem  7302  oeeui  7303  oaabs2  7346  omabs  7348  ercl  7374  erth  7408  ecelqsdm  7433  ordtypelem6  8036  ordtypelem7  8037  cantnfval  8170  cantnfp1lem3  8182  cantnflem4  8194  r1pwss  8252  rankonidlem  8296  rankxplim3  8349  fseqenlem2  8452  iunfictbso  8541  dfac12lem1  8569  dfac12lem2  8570  fin23lem30  8768  iundom2g  8961  fpwwe2lem6  9056  fpwwe2lem9  9059  lincmb01cmp  11769  fzopth  11829  fzoaddel2  11963  fzosubel2  11967  fzocatel  11971  zpnn0elfzo1  11980  fzoend  11995  peano2fzor  12009  monoord2  12237  sermono  12238  expmulnbnd  12397  bcpasc  12499  swrdcl  12756  revcl  12847  revlen  12848  fsum0diag2  13822  isumsplit  13876  fprodser  13981  sadadd  14419  sadass  14423  smuval2  14434  smumul  14445  vdwapun  14902  vdwlem9  14917  ramub1lem1  14962  prdsbasfn  15347  prdsbasprj  15348  pwsplusgval  15366  pwsmulrval  15367  pwsvscafval  15370  xpsaddlem  15459  xpsvsca  15463  xpsle  15465  mreexmrid  15527  homfeqval  15580  comfval2  15586  comfeq  15589  comfeqval  15591  oppccomfpropd  15610  invco  15654  sectepi  15667  issubc3  15732  funcf2  15751  funciso  15757  fthepi  15811  nat1st2nd  15834  fuciso  15858  homarcl2  15908  coapm  15944  setcmon  15960  setcepi  15961  setcsect  15962  setcinv  15963  setciso  15964  catccatid  15975  resscatc  15978  catciso  15980  catcoppccl  15981  catcfuccl  15982  xpccatid  16051  catcxpccl  16070  xpcpropd  16071  evlfcl  16085  curfpropd  16096  hofcl  16122  yonedalem3  16143  yonffthlem  16145  poslubdg  16373  grpidd  16489  gsumress  16497  ismndd  16537  mndpropd  16540  issubmnd  16542  submnd0  16544  imasmnd  16552  frmdelbas  16615  grpidd2  16681  submmulg  16771  pwsinvg  16776  imasgrp  16780  subginvcl  16804  subgcl  16805  subgsub  16807  subgmulg  16809  quseccl  16851  gaid2  16935  submod  17196  odsubdvds  17198  sylow1lem4  17231  sylow2alem2  17248  lsmdisj2  17310  subgdisj1  17319  pj1id  17327  efgsrel  17362  efgrelexlemb  17378  efgcpbl2  17385  frgpcpbl  17387  frgp0  17388  frgpeccl  17389  frgpadd  17391  frgpup3lem  17405  frgpnabllem1  17487  cycsubgcyg  17513  prdsgsum  17588  dprdfeq0  17633  dmdprdsplitlem  17648  dpjidcl  17669  pgpfac1lem3a  17687  pgpfac1lem4  17689  pgpfaclem1  17692  pgpfaclem2  17693  ablfaclem2  17697  ringidss  17785  ringpropd  17790  imasring  17825  qusring2  17826  kerf1hrm  17949  subrg1  17996  subrgmcl  17998  subrgdv  18003  subrgunit  18004  issubdrg  18011  resrhm  18015  lmodprop2d  18128  0lmhm  18241  lmhmpropd  18274  lspfixed  18329  lssacsex  18345  lbsextlem4  18362  quscrng  18442  assapropd  18529  psrelbas  18581  resspsrvsca  18620  subrgpsr  18621  mplcoe1  18667  mplbas2  18672  mplascl  18697  mplmon2cl  18701  mplmon2mul  18702  evlrhm  18726  mpfconst  18731  vr1cl2  18764  ply1lss  18767  ply1subrg  18768  psropprmul  18809  evl1vsd  18910  evl1expd  18911  evl1gsumadd  18924  evl1gsummon  18931  znf1o  19099  psgnghm2  19126  elocv  19208  pjff  19252  frlmlss  19291  frlmsubgval  19304  frlmvscafval  19305  frlmphl  19316  uvcresum  19328  frlmssuvc1  19329  frlmssuvc2  19330  frlmsslsp  19331  frlmup1  19333  matring  19445  matassa  19446  mat1  19449  mattposcl  19455  mavmulass  19551  mdetunilem9  19622  matinv  19679  cpmadugsumlemF  19877  cpmadugsumfi  19878  cpmidgsum2  19880  elcls3  20076  mreclatdemoBAD  20089  neiptopnei  20125  resstps  20180  ordtrest2lem  20196  ordtrest2  20197  pnfnei  20213  mnfnei  20214  iscnp2  20232  iscnp4  20256  cnrest2r  20280  lmcls  20295  lmcld  20296  cnt0  20339  cnhaus  20347  isreg2  20370  conclo  20407  1stccnp  20454  loclly  20479  lly1stc  20488  locfincmp  20518  unisngl  20519  comppfsc  20524  kgencmp2  20538  llycmpkgen2  20542  kgen2ss  20547  kgencn3  20550  pttoponconst  20589  txcls  20596  txbasval  20598  dfac14lem  20609  ptcn  20619  ptrescn  20631  txtube  20632  txcmplem1  20633  txlm  20640  txkgen  20644  xkopjcn  20648  cnmptkp  20672  xkoinjcn  20679  qtopkgen  20702  imastps  20713  isr0  20729  r0cld  20730  pt1hmeo  20798  ptuncnv  20799  ptunhmeo  20800  filintn0  20853  trnei  20884  flimfil  20961  flimopn  20967  fbflim2  20969  cnpflf2  20992  flfcnp  20996  flfcnp2  20999  fclsopn  21006  fcfnei  21027  cnpfcf  21033  flfcntr  21035  alexsublem  21036  ptcmplem3  21046  ptcmplem4  21047  cnextfres1  21060  tmdcn2  21081  tmdgsum  21087  tmdgsum2  21088  symgtgp  21093  tgphaus  21108  tgpt1  21109  qustgplem  21112  prdstmdd  21115  prdstgpd  21116  haustsms  21127  tsmscls  21129  tsmsmhm  21137  tsmsadd  21138  tgptsmscls  21141  tsmssplit  21143  restutop  21229  utopreg  21244  ressusp  21257  ucncn  21277  xmetunirn  21329  ressprdsds  21363  xpsdsval  21373  xblss2ps  21393  blbas  21422  mopntopon  21431  isxms2  21440  imasf1oxms  21481  imasf1oms  21482  prdsxmslem2  21521  tmsxpsval  21530  tngngp2  21637  tngngp  21639  tgioo  21791  metdseq0  21848  metdseq0OLD  21863  cncfmpt2f  21923  cncfcnvcn  21930  cnmptre  21932  cnheibor  21960  nmhmcn  22111  cvsdiv  22117  cvsdivcl  22118  cphsubrglem  22132  cphreccllem  22133  iscmet3  22240  relcmpcmet  22263  bcthlem4  22272  rrxds  22329  minveclem4  22351  minveclem4OLD  22363  ivthicc  22386  evthicc  22387  ovolicc2lem4OLD  22450  ovolicc2lem4  22451  ovolicc2lem5  22452  iunmbl2  22487  vitalilem3  22545  cncombf  22591  cnmbf  22592  dvres2lem  22842  cpncn  22867  cpnres  22868  dvaddbr  22869  dvmulbr  22870  dvcobr  22877  dvcjbr  22880  dvrec  22886  dvcnvlem  22905  dvlip2  22924  dvivth  22939  lhop2  22944  lhop  22945  dvcnvrelem1  22946  dvcnvrelem2  22947  dvcnvre  22948  ftc1lem6  22970  mdegvscale  23001  mdegvsca  23002  fta1blem  23096  plyaddlem1  23144  plymullem1  23145  coeeulem  23155  tayl0  23294  taylthlem1  23305  taylthlem2  23306  ulmdvlem3  23334  psercnlem2  23356  psercn  23358  efsubm  23477  cxpcn3  23665  loglesqrt  23675  efrlim  23872  ppinprm  24056  chtnprm  24058  dchrptlem1  24169  dchrptlem2  24170  tgbtwnouttr2  24516  tgldim0eq  24524  tgifscgr  24530  iscgrglt  24536  ercgrg  24539  tgcgrxfr  24540  motcgrg  24566  tglngne  24572  tgcolg  24576  tgbtwnconn1lem2  24595  tgbtwnconn1lem3  24596  legtri3  24612  legbtwn  24616  ncolne1  24647  tgisline  24649  tglinethru  24658  coltr3  24670  colline  24671  tglowdim2ln  24673  mirinv  24688  miriso  24692  mirauto  24706  miduniq  24707  krippenlem  24712  midexlem  24714  ragperp  24739  footex  24740  perpdragALT  24746  perpdrag  24747  colperpexlem1  24749  colperpexlem3  24751  mideulem2  24753  midex  24756  opphllem1  24766  opphllem3  24768  opphllem4  24769  hlpasch  24775  trgcopy  24823  acopyeu  24852  f1otrg  24878  axlowdimlem16  24964  elntg  24991  eengtrkg  24992  eengtrkge  24993  eupap1  25680  grpoidinv2  25922  grpoinv  25931  ubthlem2  26489  shuni  26929  acunirnmpt  28242  acunirnmpt2  28243  acunirnmpt2f  28244  fpwrelmap  28303  gsummpt2d  28532  rngurd  28540  ordtrest2NEWlem  28717  ordtrest2NEW  28718  lmxrge0  28747  nmmulg  28761  rrhcn  28790  esumadd  28867  esumaddf  28871  esumcocn  28890  measiuns  29028  mbfmco2  29076  dya2iocnrect  29092  omscl  29108  omsf  29109  omsclOLD  29112  omsfOLD  29113  oms0  29114  oms0OLD  29118  sibf0  29156  sibfof  29162  sitgaddlemb  29170  fibp1  29223  ccatmulgnn0dir  29417  bnj1450  29848  bnj1501  29865  indispcon  29946  conpcon  29947  pconpi1  29949  sconpi1  29951  cvmsss2  29986  cvmliftmolem1  29993  cvmliftlem8  30004  cvmliftlem10  30006  cvmliftlem11  30007  cvmlift2lem9  30023  cvmlift2lem12  30026  cvmlift3lem7  30037  mrsubcv  30137  mrsubff  30139  mrsubccat  30145  elmrsubrn  30147  mrsubco  30148  mrsubvrs  30149  linethru  30906  ivthALT  30977  neibastop2  31003  filnetlem4  31023  poimirlem1  31849  poimirlem2  31850  poimirlem8  31856  poimirlem9  31857  poimirlem16  31864  poimirlem17  31865  poimirlem19  31867  poimirlem20  31868  poimirlem22  31870  poimirlem23  31871  poimir  31881  broucube  31882  areacirclem4  31943  fdc  31982  isbnd3  32024  prdsbnd  32033  prdstotbnd  32034  prdsbnd2  32035  rrnequiv  32075  reheibor  32079  iscringd  32140  isfldidl  32209  eqlkr  32578  ldualvsubval  32636  dvalveclem  34506  dia2dimlem5  34549  dia2dimlem9  34553  tendoinvcl  34585  dvhgrp  34588  dvhlveclem  34589  dihpN  34817  dochsnkr2cl  34955  lcfl7lem  34980  lclkr  35014  lclkrs  35020  lcfrvalsnN  35022  lcfrlem4  35026  lcfrlem6  35028  lcfrlem16  35039  lcdvsubval  35099  lcdlkreqN  35103  mapdcl2  35137  mapdincl  35142  mapdlsmcl  35144  mapdpglem3  35156  hdmaprnlem9N  35341  hdmaplkr  35397  hdmapip0  35399  hdmapglem7a  35411  diophin  35528  acongeq  35747  isnumbasgrplem2  35877  proot1mul  35987  iunrelexpuztr  36165  bccbc  36546  suctrALT  37077  disjf1o  37304  disjinfi  37306  monoords  37338  elfzolem1  37368  uzfissfz  37373  evthiccabs  37393  iooabslt  37396  islptre  37486  limciccioolb  37488  sumnnodd  37497  limcicciooub  37504  lptre2pt  37507  limcresiooub  37510  limcresioolb  37511  lptioo1cn  37514  reclimc  37521  fsumcncf  37542  ioccncflimc  37550  cncfuni  37551  icccncfext  37552  cncficcgt0  37553  icocncflimc  37554  cncfdmsn  37555  cncfiooicclem1  37558  cncfiooicc  37559  cncfioobd  37562  cxpcncf2  37565  fperdvper  37577  dvcosax  37585  dvnmul  37605  dvnprodlem1  37608  dvnprodlem2  37609  itgsubsticclem  37639  stoweidlem26  37673  stoweidlem27  37674  stoweidlem31  37679  stoweidlem34  37682  dirkercncflem2  37753  dirkercncflem3  37754  dirkercncflem4  37755  dirkercncf  37756  fourierdlem16  37772  fourierdlem20  37776  fourierdlem21  37777  fourierdlem22  37778  fourierdlem26  37782  fourierdlem32  37789  fourierdlem33  37790  fourierdlem38  37795  fourierdlem39  37796  fourierdlem46  37803  fourierdlem48  37805  fourierdlem49  37806  fourierdlem53  37810  fourierdlem60  37817  fourierdlem61  37818  fourierdlem69  37826  fourierdlem70  37827  fourierdlem71  37828  fourierdlem73  37830  fourierdlem74  37831  fourierdlem75  37832  fourierdlem76  37833  fourierdlem80  37837  fourierdlem81  37838  fourierdlem82  37839  fourierdlem83  37840  fourierdlem84  37841  fourierdlem85  37842  fourierdlem88  37845  fourierdlem89  37846  fourierdlem91  37848  fourierdlem92  37849  fourierdlem93  37850  fourierdlem100  37857  fourierdlem101  37858  fourierdlem103  37860  fourierdlem104  37861  fourierdlem107  37864  fourierdlem111  37868  fourierdlem112  37869  fourierdlem113  37870  fouriersw  37882  fouriercn  37883  etransclem24  37910  etransclem26  37912  etransclem28  37914  etransclem31  37917  etransclem32  37918  etransclem33  37919  etransclem34  37920  etransclem35  37921  etransclem38  37924  prsal  37947  intsaluni  37956  fge0iccico  37967  sge0sn  37976  sge0tsms  37977  sge0cl  37978  sge0f1o  37979  sge0pr  37991  nnfoctbdjlem  38023  iundjiunlem  38027  iundjiun  38028  meadjiunlem  38033  psmeasure  38039  caragenelss  38052  omeunile  38056  carageniuncllem1  38072  carageniuncllem2  38073  fzoopth  38659  issubmgm2  38852  zlmodzxzel  39200  ply1mulgsum  39246