Theorem eleqtrd 2557

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

Syntax hints:   -> wi 4   = wceq 1379   e. wcel 1767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462

This theorem is referenced by:  eleqtrrd  2558  syl5eleq  2561  syl6eleq  2565  3eltr3d  2569  opth1  4720  0nelop  4737  fviss  5924  tfisi  6672  fnwelem  6898  omeulem1  7231  oeeulem  7250  oeeui  7251  oaabs2  7294  omabs  7296  ercl  7322  erth  7356  ecelqsdm  7381  ordtypelem6  7947  ordtypelem7  7948  cantnfval  8086  cantnfp1lem3  8098  cantnflem4  8110  cantnfvalOLD  8116  cantnfp1lem3OLD  8124  cantnflem4OLD  8132  r1pwss  8201  rankonidlem  8245  rankxplim3  8298  fseqenlem2  8405  iunfictbso  8494  dfac12lem1  8522  dfac12lem2  8523  fin23lem30  8721  iundom2g  8914  fpwwe2lem6  9012  fpwwe2lem9  9015  lincmb01cmp  11662  fzopth  11719  fzoaddel2  11841  fzosubel2  11843  fzocatel  11847  zpnn0elfzo1  11856  fzoend  11870  peano2fzor  11884  monoord2  12105  sermono  12106  expmulnbnd  12265  bcpasc  12366  ccatcl  12557  ccatw2s1p2  12603  swrdcl  12608  revcl  12697  revlen  12698  fsum0diag2  13560  isumsplit  13614  sadadd  13975  sadass  13979  smuval2  13990  smumul  14001  vdwapun  14350  vdwlem9  14365  ramub1lem1  14402  prdsbasfn  14725  prdsbasprj  14726  pwsplusgval  14744  pwsmulrval  14745  pwsvscafval  14748  xpsaddlem  14829  xpsvsca  14833  xpsle  14835  mreexmrid  14897  homfeqval  14952  comfval2  14958  comfeq  14961  comfeqval  14963  oppccomfpropd  14982  invco  15025  sectepi  15034  issubc3  15075  funcf2  15094  funciso  15100  fthepi  15154  nat1st2nd  15177  fuciso  15201  homarcl2  15219  coapm  15255  setcmon  15271  setcepi  15272  setcsect  15273  setcinv  15274  setciso  15275  catccatid  15286  resscatc  15289  catciso  15291  catcoppccl  15292  catcfuccl  15293  xpccatid  15314  catcxpccl  15333  xpcpropd  15334  evlfcl  15348  curfpropd  15359  hofcl  15385  yonedalem3  15406  yonffthlem  15408  poslubdg  15635  grpidd  15759  ismndd  15760  mndpropd  15763  issubmnd  15766  submnd0  15768  imasmnd  15776  gsumress  15826  frmdelbas  15850  grpidd2  15894  submmulg  15984  pwsinvg  15989  imasgrp  15993  subginvcl  16012  subgcl  16013  subgsub  16015  subgmulg  16017  divseccl  16059  gaid2  16143  submod  16392  odsubdvds  16394  sylow1lem4  16424  sylow2alem2  16441  lsmdisj2  16503  subgdisj1  16512  pj1id  16520  efgsrel  16555  efgrelexlemb  16571  efgcpbl2  16578  frgpcpbl  16580  frgp0  16581  frgpeccl  16582  frgpadd  16584  frgpup3lem  16598  frgpnabllem1  16677  cycsubgcyg  16703  prdsgsum  16807  prdsgsumOLD  16808  dprdfeq0  16861  dprdfeq0OLD  16868  dmdprdsplitlem  16883  dmdprdsplitlemOLD  16884  dpjidcl  16906  dpjidclOLD  16913  pgpfac1lem3a  16926  pgpfac1lem4  16928  pgpfaclem1  16931  pgpfaclem2  16932  ablfaclem2  16936  rngidss  17021  rngpropd  17026  imasrng  17064  divsrng2  17065  kerf1hrm  17187  subrg1  17234  subrgmcl  17236  subrgdv  17241  subrgunit  17242  issubdrg  17249  resrhm  17253  lmodprop2d  17367  0lmhm  17481  lmhmpropd  17514  lspfixed  17569  lssacsex  17585  lbsextlem4  17602  divscrng  17682  assapropd  17763  psrelbas  17819  resspsrvsca  17860  subrgpsr  17861  mplcoe1  17914  mplbas2  17921  mplbas2OLD  17922  mplascl  17948  mplmon2cl  17952  mplmon2mul  17953  evlrhm  17981  mpfconst  17986  vr1cl2  18019  ply1lss  18022  ply1subrg  18023  psropprmul  18066  evl1vsd  18167  evl1expd  18168  evl1gsumadd  18181  evl1gsummon  18188  znf1o  18373  psgnghm2  18400  elocv  18482  pjff  18526  frlmlss  18565  frlmsubgval  18581  frlmvscafval  18582  frlmphl  18595  uvcresum  18607  frlmssuvc1  18608  frlmssuvc2  18609  frlmssuvc1OLD  18610  frlmssuvc2OLD  18611  frlmsslsp  18612  frlmsslspOLD  18613  frlmup1  18615  matrng  18728  matassa  18729  mat1  18732  mattposcl  18738  mavmulass  18834  mdetunilem9  18905  matinv  18962  cpmadugsumlemF  19160  cpmadugsumfi  19161  cpmidgsum2  19163  elcls3  19366  mreclatdemoBAD  19379  neiptopnei  19415  resstps  19470  ordtrest2lem  19486  ordtrest2  19487  pnfnei  19503  mnfnei  19504  iscnp2  19522  iscnp4  19546  cnrest2r  19570  lmcls  19585  lmcld  19586  cnt0  19629  cnhaus  19637  isreg2  19660  conclo  19698  1stccnp  19745  loclly  19770  lly1stc  19779  kgencmp2  19798  llycmpkgen2  19802  kgen2ss  19807  kgencn3  19810  pttoponconst  19849  txcls  19856  txbasval  19858  dfac14lem  19869  ptcn  19879  ptrescn  19891  txtube  19892  txcmplem1  19893  txlm  19900  txkgen  19904  xkopjcn  19908  cnmptkp  19932  xkoinjcn  19939  qtopkgen  19962  imastps  19973  isr0  19989  r0cld  19990  pt1hmeo  20058  ptuncnv  20059  ptunhmeo  20060  filintn0  20113  trnei  20144  flimfil  20221  flimopn  20227  fbflim2  20229  cnpflf2  20252  flfcnp  20256  flfcnp2  20259  fclsopn  20266  fcfnei  20287  cnpfcf  20293  alexsublem  20295  ptcmplem3  20305  ptcmplem4  20306  cnextfres  20319  tmdcn2  20339  tmdgsum  20345  tmdgsum2  20346  symgtgp  20351  tgphaus  20366  tgpt1  20367  divstgplem  20370  prdstmdd  20373  prdstgpd  20374  haustsms  20385  tsmscls  20387  tsmsmhm  20399  tsmsadd  20400  tgptsmscls  20403  tsmssplit  20405  restutop  20491  utopreg  20506  ressusp  20519  ucncn  20539  xmetunirn  20591  ressprdsds  20625  xpsdsval  20635  xblss2ps  20655  blbas  20684  mopntopon  20693  isxms2  20702  imasf1oxms  20743  imasf1oms  20744  prdsxmslem2  20783  tmsxpsval  20792  tngngp2  20917  tngngp  20919  tgioo  21052  metdseq0  21109  cncfmpt2f  21169  cncfcnvcn  21176  cnmptre  21178  cnheibor  21206  nmhmcn  21354  cvsdiv  21360  cvsdivcl  21361  cphsubrglem  21375  cphreccllem  21376  iscmet3  21483  relcmpcmet  21506  bcthlem4  21517  rrxds  21576  minveclem4  21598  ivthicc  21621  evthicc  21622  ovolicc2lem4  21682  ovolicc2lem5  21683  iunmbl2  21718  vitalilem3  21770  cncombf  21816  cnmbf  21817  dvres2lem  22065  cpncn  22090  cpnres  22091  dvaddbr  22092  dvmulbr  22093  dvcobr  22100  dvcjbr  22103  dvrec  22109  dvcnvlem  22128  dvlip2  22147  dvivth  22162  lhop2  22167  lhop  22168  dvcnvrelem1  22169  dvcnvrelem2  22170  dvcnvre  22171  ftc1lem6  22193  mdegvscale  22226  mdegvsca  22227  fta1blem  22320  plyaddlem1  22361  plymullem1  22362  coeeulem  22372  tayl0  22507  taylthlem1  22518  taylthlem2  22519  ulmdvlem3  22547  psercnlem2  22569  psercn  22571  cxpcn3  22866  loglesqrt  22876  efrlim  23043  ppinprm  23170  chtnprm  23172  dchrptlem1  23283  dchrptlem2  23284  tgbtwnouttr2  23630  tgldim0eq  23638  tgifscgr  23644  ercgrg  23652  tgcgrxfr  23653  motcgrg  23675  tgcolg  23685  tgbtwnconn1lem2  23703  tgbtwnconn1lem3  23704  legtri3  23720  legbtwn  23724  ncolne1  23735  tgisline  23737  tglinethru  23746  coltr3  23758  colline  23759  tglowdim2ln  23761  mirinv  23776  miriso  23779  mirauto  23785  miduniq  23786  krippenlem  23791  midexlem  23793  ragperp  23818  footex  23819  perpdragALT  23822  perpdrag  23823  colperpexlem1  23825  colperpexlem3  23827  mideulem  23829  mideu  23830  f1otrg  23866  axlowdimlem16  23952  elntg  23979  eengtrkg  23980  eengtrkge  23981  eupap1  24668  grpoidinv2  24912  grpoinv  24921  ubthlem2  25479  shuni  25910  fpwrelmap  27244  rngurd  27457  txomap  27516  ordtrest2NEWlem  27556  ordtrest2NEW  27557  lmxrge0  27586  nmmulg  27601  rrhcn  27630  esumadd  27720  esumaddf  27725  esumcocn  27742  measiuns  27844  mbfmco2  27892  dya2iocnrect  27908  oms0  27922  sibf0  27932  sibfof  27938  fibp1  27996  ccatmulgnn0dir  28152  indispcon  28335  conpcon  28336  pconpi1  28338  sconpi1  28340  cvmsss2  28375  cvmliftmolem1  28382  cvmliftlem8  28393  cvmliftlem10  28395  cvmliftlem11  28396  cvmlift2lem9  28412  cvmlift2lem12  28415  cvmlift3lem7  28426  fprodser  28674  linethru  29396  areacirclem4  29703  ivthALT  29746  locfincmp  29792  comppfsc  29795  neibastop2  29798  filnetlem4  29818  fdc  29857  isbnd3  29899  prdsbnd  29908  prdstotbnd  29909  prdsbnd2  29910  rrnequiv  29950  reheibor  29954  iscringd  30015  isfldidl  30084  diophin  30326  acongeq  30541  isnumbasgrplem2  30673  proot1mul  30777  monoords  31089  evthiccabs  31109  iooabslt  31112  islptre  31177  limciccioolb  31179  sumnnodd  31188  limcicciooub  31195  lptre2pt  31198  limcresiooub  31200  limcresioolb  31201  lptioo1cn  31204  reclimc  31211  fsumcncf  31232  ioccncflimc  31240  cncfuni  31241  icccncfext  31242  cncficcgt0  31243  icocncflimc  31244  cncfdmsn  31245  cncfshiftioo  31247  cncfiooicclem1  31248  cncfiooicc  31249  cncfioobd  31252  fperdvper  31264  dvcosax  31272  ditgeqiooicc  31294  itgsubsticclem  31309  itgperiod  31315  stoweidlem26  31342  stoweidlem27  31343  stoweidlem31  31347  stoweidlem34  31350  dirkertrigeqlem2  31415  dirkertrigeqlem3  31416  dirkercncflem2  31420  dirkercncflem3  31421  dirkercncflem4  31422  dirkercncf  31423  fourierdlem11  31434  fourierdlem15  31438  fourierdlem16  31439  fourierdlem20  31443  fourierdlem21  31444  fourierdlem22  31445  fourierdlem32  31455  fourierdlem33  31456  fourierdlem38  31461  fourierdlem39  31462  fourierdlem41  31464  fourierdlem42  31465  fourierdlem46  31469  fourierdlem48  31471  fourierdlem49  31472  fourierdlem51  31474  fourierdlem53  31476  fourierdlem58  31481  fourierdlem60  31483  fourierdlem61  31484  fourierdlem62  31485  fourierdlem63  31486  fourierdlem64  31487  fourierdlem69  31492  fourierdlem70  31493  fourierdlem71  31494  fourierdlem73  31496  fourierdlem74  31497  fourierdlem75  31498  fourierdlem76  31499  fourierdlem80  31503  fourierdlem81  31504  fourierdlem82  31505  fourierdlem83  31506  fourierdlem84  31507  fourierdlem85  31508  fourierdlem88  31511  fourierdlem89  31512  fourierdlem91  31514  fourierdlem92  31515  fourierdlem93  31516  fourierdlem97  31520  fourierdlem100  31523  fourierdlem101  31524  fourierdlem102  31525  fourierdlem103  31526  fourierdlem104  31527  fourierdlem107  31530  fourierdlem111  31534  fourierdlem112  31535  fourierdlem113  31536  fourierdlem114  31537  fouriercnp  31543  fouriersw  31548  fouriercn  31549  el2fzo  31822  fzoopth  31823  zlmodzxzel  32028  ply1mulgsum  32080  suctrALT  32715  bnj1450  33194  bnj1501  33211  eqlkr  33905  ldualvsubval  33963  dvalveclem  35831  dia2dimlem5  35874  dia2dimlem9  35878  tendoinvcl  35910  dvhgrp  35913  dvhlveclem  35914  dihpN  36142  dochsnkr2cl  36280  lcfl7lem  36305  lclkr  36339  lclkrs  36345  lcfrvalsnN  36347  lcfrlem4  36351  lcfrlem6  36353  lcfrlem16  36364  lcdvsubval  36424  lcdlkreqN  36428  mapdcl2  36462  mapdincl  36467  mapdlsmcl  36469  mapdpglem3  36481  hdmaprnlem9N  36666  hdmaplkr  36722  hdmapip0  36724  hdmapglem7a  36736