Theorem eleqtrd 2530

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

Syntax hints:   -> wi 4   = wceq 1443   e. wcel 1886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1663  df-cleq 2443  df-clel 2446

This theorem is referenced by:  eleqtrrd  2531  syl5eleq  2534  syl6eleq  2538  3eltr3d  2542  opth1  4674  0nelop  4690  fviss  5921  tfisi  6682  fnwelem  6908  wfrlem17  7049  omeulem1  7280  oeeulem  7299  oeeui  7300  oaabs2  7343  omabs  7345  ercl  7371  erth  7405  ecelqsdm  7430  ordtypelem6  8035  ordtypelem7  8036  cantnfval  8170  cantnfp1lem3  8182  cantnflem4  8194  r1pwss  8252  rankonidlem  8296  rankxplim3  8349  fseqenlem2  8453  iunfictbso  8542  dfac12lem1  8570  dfac12lem2  8571  fin23lem30  8769  iundom2g  8962  fpwwe2lem6  9057  fpwwe2lem9  9060  lincmb01cmp  11772  fzopth  11832  fzoaddel2  11967  fzosubel2  11971  fzocatel  11975  zpnn0elfzo1  11984  fzoend  11999  peano2fzor  12013  monoord2  12241  sermono  12242  expmulnbnd  12401  bcpasc  12503  swrdcl  12770  revcl  12861  revlen  12862  fsum0diag2  13837  isumsplit  13891  fprodser  13996  sadadd  14434  sadass  14438  smuval2  14449  smumul  14460  vdwapun  14917  vdwlem9  14932  ramub1lem1  14977  prdsbasfn  15362  prdsbasprj  15363  pwsplusgval  15381  pwsmulrval  15382  pwsvscafval  15385  xpsaddlem  15474  xpsvsca  15478  xpsle  15480  mreexmrid  15542  homfeqval  15595  comfval2  15601  comfeq  15604  comfeqval  15606  oppccomfpropd  15625  invco  15669  sectepi  15682  issubc3  15747  funcf2  15766  funciso  15772  fthepi  15826  nat1st2nd  15849  fuciso  15873  homarcl2  15923  coapm  15959  setcmon  15975  setcepi  15976  setcsect  15977  setcinv  15978  setciso  15979  catccatid  15990  resscatc  15993  catciso  15995  catcoppccl  15996  catcfuccl  15997  xpccatid  16066  catcxpccl  16085  xpcpropd  16086  evlfcl  16100  curfpropd  16111  hofcl  16137  yonedalem3  16158  yonffthlem  16160  poslubdg  16388  grpidd  16504  gsumress  16512  ismndd  16552  mndpropd  16555  issubmnd  16557  submnd0  16559  imasmnd  16567  frmdelbas  16630  grpidd2  16696  submmulg  16786  pwsinvg  16791  imasgrp  16795  subginvcl  16819  subgcl  16820  subgsub  16822  subgmulg  16824  quseccl  16866  gaid2  16950  submod  17211  odsubdvds  17213  sylow1lem4  17246  sylow2alem2  17263  lsmdisj2  17325  subgdisj1  17334  pj1id  17342  efgsrel  17377  efgrelexlemb  17393  efgcpbl2  17400  frgpcpbl  17402  frgp0  17403  frgpeccl  17404  frgpadd  17406  frgpup3lem  17420  frgpnabllem1  17502  cycsubgcyg  17528  prdsgsum  17603  dprdfeq0  17648  dmdprdsplitlem  17663  dpjidcl  17684  pgpfac1lem3a  17702  pgpfac1lem4  17704  pgpfaclem1  17707  pgpfaclem2  17708  ablfaclem2  17712  ringidss  17800  ringpropd  17805  imasring  17840  qusring2  17841  kerf1hrm  17964  subrg1  18011  subrgmcl  18013  subrgdv  18018  subrgunit  18019  issubdrg  18026  resrhm  18030  lmodprop2d  18143  0lmhm  18256  lmhmpropd  18289  lspfixed  18344  lssacsex  18360  lbsextlem4  18377  quscrng  18457  assapropd  18544  psrelbas  18596  resspsrvsca  18635  subrgpsr  18636  mplcoe1  18682  mplbas2  18687  mplascl  18712  mplmon2cl  18716  mplmon2mul  18717  evlrhm  18741  mpfconst  18746  vr1cl2  18779  ply1lss  18782  ply1subrg  18783  psropprmul  18824  evl1vsd  18925  evl1expd  18926  evl1gsumadd  18939  evl1gsummon  18946  znf1o  19115  psgnghm2  19142  elocv  19224  pjff  19268  frlmlss  19307  frlmsubgval  19320  frlmvscafval  19321  frlmphl  19332  uvcresum  19344  frlmssuvc1  19345  frlmssuvc2  19346  frlmsslsp  19347  frlmup1  19349  matring  19461  matassa  19462  mat1  19465  mattposcl  19471  mavmulass  19567  mdetunilem9  19638  matinv  19695  cpmadugsumlemF  19893  cpmadugsumfi  19894  cpmidgsum2  19896  elcls3  20092  mreclatdemoBAD  20105  neiptopnei  20141  resstps  20196  ordtrest2lem  20212  ordtrest2  20213  pnfnei  20229  mnfnei  20230  iscnp2  20248  iscnp4  20272  cnrest2r  20296  lmcls  20311  lmcld  20312  cnt0  20355  cnhaus  20363  isreg2  20386  conclo  20423  1stccnp  20470  loclly  20495  lly1stc  20504  locfincmp  20534  unisngl  20535  comppfsc  20540  kgencmp2  20554  llycmpkgen2  20558  kgen2ss  20563  kgencn3  20566  pttoponconst  20605  txcls  20612  txbasval  20614  dfac14lem  20625  ptcn  20635  ptrescn  20647  txtube  20648  txcmplem1  20649  txlm  20656  txkgen  20660  xkopjcn  20664  cnmptkp  20688  xkoinjcn  20695  qtopkgen  20718  imastps  20729  isr0  20745  r0cld  20746  pt1hmeo  20814  ptuncnv  20815  ptunhmeo  20816  filintn0  20869  trnei  20900  flimfil  20977  flimopn  20983  fbflim2  20985  cnpflf2  21008  flfcnp  21012  flfcnp2  21015  fclsopn  21022  fcfnei  21043  cnpfcf  21049  flfcntr  21051  alexsublem  21052  ptcmplem3  21062  ptcmplem4  21063  cnextfres1  21076  tmdcn2  21097  tmdgsum  21103  tmdgsum2  21104  symgtgp  21109  tgphaus  21124  tgpt1  21125  qustgplem  21128  prdstmdd  21131  prdstgpd  21132  haustsms  21143  tsmscls  21145  tsmsmhm  21153  tsmsadd  21154  tgptsmscls  21157  tsmssplit  21159  restutop  21245  utopreg  21260  ressusp  21273  ucncn  21293  xmetunirn  21345  ressprdsds  21379  xpsdsval  21389  xblss2ps  21409  blbas  21438  mopntopon  21447  isxms2  21456  imasf1oxms  21497  imasf1oms  21498  prdsxmslem2  21537  tmsxpsval  21546  tngngp2  21653  tngngp  21655  tgioo  21807  metdseq0  21864  metdseq0OLD  21879  cncfmpt2f  21939  cncfcnvcn  21946  cnmptre  21948  cnheibor  21976  nmhmcn  22127  cvsdiv  22133  cvsdivcl  22134  cphsubrglem  22148  cphreccllem  22149  iscmet3  22256  relcmpcmet  22279  bcthlem4  22288  rrxds  22345  minveclem4  22367  minveclem4OLD  22379  ivthicc  22402  evthicc  22403  ovolicc2lem4OLD  22466  ovolicc2lem4  22467  ovolicc2lem5  22468  iunmbl2  22503  vitalilem3  22561  cncombf  22607  cnmbf  22608  dvres2lem  22858  cpncn  22883  cpnres  22884  dvaddbr  22885  dvmulbr  22886  dvcobr  22893  dvcjbr  22896  dvrec  22902  dvcnvlem  22921  dvlip2  22940  dvivth  22955  lhop2  22960  lhop  22961  dvcnvrelem1  22962  dvcnvrelem2  22963  dvcnvre  22964  ftc1lem6  22986  mdegvscale  23017  mdegvsca  23018  fta1blem  23112  plyaddlem1  23160  plymullem1  23161  coeeulem  23171  tayl0  23310  taylthlem1  23321  taylthlem2  23322  ulmdvlem3  23350  psercnlem2  23372  psercn  23374  efsubm  23493  cxpcn3  23681  loglesqrt  23691  efrlim  23888  ppinprm  24072  chtnprm  24074  dchrptlem1  24185  dchrptlem2  24186  tgbtwnouttr2  24532  tgldim0eq  24540  tgifscgr  24546  iscgrglt  24552  ercgrg  24555  tgcgrxfr  24556  motcgrg  24582  tglngne  24588  tgcolg  24592  tgbtwnconn1lem2  24611  tgbtwnconn1lem3  24612  legtri3  24628  legbtwn  24632  ncolne1  24663  tgisline  24665  tglinethru  24674  coltr3  24686  colline  24687  tglowdim2ln  24689  mirinv  24704  miriso  24708  mirauto  24722  miduniq  24723  krippenlem  24728  midexlem  24730  ragperp  24755  footex  24756  perpdragALT  24762  perpdrag  24763  colperpexlem1  24765  colperpexlem3  24767  mideulem2  24769  midex  24772  opphllem1  24782  opphllem3  24784  opphllem4  24785  hlpasch  24791  trgcopy  24839  acopyeu  24868  f1otrg  24894  axlowdimlem16  24980  elntg  25007  eengtrkg  25008  eengtrkge  25009  eupap1  25697  grpoidinv2  25939  grpoinv  25948  ubthlem2  26506  shuni  26946  acunirnmpt  28254  acunirnmpt2  28255  acunirnmpt2f  28256  fpwrelmap  28311  gsummpt2d  28537  rngurd  28544  ordtrest2NEWlem  28721  ordtrest2NEW  28722  lmxrge0  28751  nmmulg  28765  rrhcn  28794  esumadd  28871  esumaddf  28875  esumcocn  28894  measiuns  29032  mbfmco2  29080  dya2iocnrect  29096  omscl  29112  omsf  29113  omsclOLD  29116  omsfOLD  29117  oms0  29118  oms0OLD  29122  sibf0  29160  sibfof  29166  sitgaddlemb  29174  fibp1  29227  ccatmulgnn0dir  29421  bnj1450  29852  bnj1501  29869  indispcon  29950  conpcon  29951  pconpi1  29953  sconpi1  29955  cvmsss2  29990  cvmliftmolem1  29997  cvmliftlem8  30008  cvmliftlem10  30010  cvmliftlem11  30011  cvmlift2lem9  30027  cvmlift2lem12  30030  cvmlift3lem7  30041  mrsubcv  30141  mrsubff  30143  mrsubccat  30149  elmrsubrn  30151  mrsubco  30152  mrsubvrs  30153  linethru  30913  ivthALT  30984  neibastop2  31010  filnetlem4  31030  poimirlem1  31934  poimirlem2  31935  poimirlem8  31941  poimirlem9  31942  poimirlem16  31949  poimirlem17  31950  poimirlem19  31952  poimirlem20  31953  poimirlem22  31955  poimirlem23  31956  poimir  31966  broucube  31967  areacirclem4  32028  fdc  32067  isbnd3  32109  prdsbnd  32118  prdstotbnd  32119  prdsbnd2  32120  rrnequiv  32160  reheibor  32164  iscringd  32225  isfldidl  32294  eqlkr  32659  ldualvsubval  32717  dvalveclem  34587  dia2dimlem5  34630  dia2dimlem9  34634  tendoinvcl  34666  dvhgrp  34669  dvhlveclem  34670  dihpN  34898  dochsnkr2cl  35036  lcfl7lem  35061  lclkr  35095  lclkrs  35101  lcfrvalsnN  35103  lcfrlem4  35107  lcfrlem6  35109  lcfrlem16  35120  lcdvsubval  35180  lcdlkreqN  35184  mapdcl2  35218  mapdincl  35223  mapdlsmcl  35225  mapdpglem3  35237  hdmaprnlem9N  35422  hdmaplkr  35478  hdmapip0  35480  hdmapglem7a  35492  diophin  35609  acongeq  35827  isnumbasgrplem2  35957  proot1mul  36067  iunrelexpuztr  36305  bccbc  36688  suctrALT  37216  disjf1o  37460  disjinfi  37462  choicefi  37475  monoords  37508  elfzolem1  37538  uzfissfz  37543  evthiccabs  37587  iooabslt  37590  islptre  37693  limciccioolb  37695  sumnnodd  37704  limcicciooub  37711  lptre2pt  37714  limcresiooub  37717  limcresioolb  37718  lptioo1cn  37721  reclimc  37728  fsumcncf  37749  ioccncflimc  37757  cncfuni  37758  icccncfext  37759  cncficcgt0  37760  icocncflimc  37761  cncfdmsn  37762  cncfiooicclem1  37765  cncfiooicc  37766  cncfioobd  37769  cxpcncf2  37772  fperdvper  37784  dvcosax  37792  dvnmul  37812  dvnprodlem1  37815  dvnprodlem2  37816  itgsubsticclem  37846  stoweidlem26  37880  stoweidlem27  37881  stoweidlem31  37886  stoweidlem34  37889  dirkercncflem2  37960  dirkercncflem3  37961  dirkercncflem4  37962  dirkercncf  37963  fourierdlem16  37979  fourierdlem20  37983  fourierdlem21  37984  fourierdlem22  37985  fourierdlem26  37989  fourierdlem32  37996  fourierdlem33  37997  fourierdlem38  38002  fourierdlem39  38003  fourierdlem46  38010  fourierdlem48  38012  fourierdlem49  38013  fourierdlem53  38017  fourierdlem60  38024  fourierdlem61  38025  fourierdlem69  38033  fourierdlem70  38034  fourierdlem71  38035  fourierdlem73  38037  fourierdlem74  38038  fourierdlem75  38039  fourierdlem76  38040  fourierdlem80  38044  fourierdlem81  38045  fourierdlem82  38046  fourierdlem83  38047  fourierdlem84  38048  fourierdlem85  38049  fourierdlem88  38052  fourierdlem89  38053  fourierdlem91  38055  fourierdlem92  38056  fourierdlem93  38057  fourierdlem100  38064  fourierdlem101  38065  fourierdlem103  38067  fourierdlem104  38068  fourierdlem107  38071  fourierdlem111  38075  fourierdlem112  38076  fourierdlem113  38077  fouriersw  38089  fouriercn  38090  etransclem24  38117  etransclem26  38119  etransclem28  38121  etransclem31  38124  etransclem32  38125  etransclem33  38126  etransclem34  38127  etransclem35  38128  etransclem38  38131  rrxbasefi  38146  rrxdsfi  38148  rrxtopnfi  38149  rrxmetfi  38150  rrxtoponfi  38154  qndenserrnbl  38158  qndenserrnopnlem  38160  qndenserrn  38162  prsal  38173  intsaluni  38182  salgencntex  38196  fge0iccico  38206  sge0sn  38215  sge0tsms  38216  sge0cl  38217  sge0f1o  38218  sge0pr  38230  sge0isum  38263  nnfoctbdjlem  38287  iundjiunlem  38291  iundjiun  38292  meadjiunlem  38297  psmeasure  38303  caragenelss  38316  omeunile  38320  carageniuncllem1  38336  carageniuncllem2  38337  0ome  38344  isomenndlem  38345  isomennd  38346  hoicvr  38364  ovnpnfelsup  38375  ovncvrrp  38380  ovnsubaddlem1  38386  hoidmv1le  38410  hoidmvlelem2  38412  hoidmvlelem3  38413  hoidmvlelem4  38414  hoidmvle  38416  ovnhoilem1  38417  hoi2toco  38423  ovncvr2  38427  hspdifhsp  38432  voncmpl  38437  hoiqssbl  38441  hspmbllem2  38443  hspmbl  38445  hoimbllem  38446  opnvonmbllem2  38449  fzoopth  39050  issubmgm2  39777  zlmodzxzel  40123  ply1mulgsum  40169