Theorem eleqtrd 2514

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

Syntax hints:   -> wi 4   = wceq 1369   e. wcel 1756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2431  df-clel 2434

This theorem is referenced by:  eleqtrrd  2515  3eltr3d  2518  syl5eleq  2524  syl6eleq  2528  opth1  4560  0nelop  4576  fviss  5744  tfisi  6464  fnwelem  6682  omeulem1  7013  oeeulem  7032  oeeui  7033  oaabs2  7076  omabs  7078  ercl  7104  erth  7137  ecelqsdm  7162  ordtypelem6  7729  ordtypelem7  7730  cantnfval  7868  cantnfp1lem3  7880  cantnflem4  7892  cantnfvalOLD  7898  cantnfp1lem3OLD  7906  cantnflem4OLD  7914  r1pwss  7983  rankonidlem  8027  rankxplim3  8080  fseqenlem2  8187  iunfictbso  8276  dfac12lem1  8304  dfac12lem2  8305  fin23lem30  8503  iundom2g  8696  fpwwe2lem6  8794  fpwwe2lem9  8797  lincmb01cmp  11420  fzopth  11487  fzoaddel2  11590  fzosubel2  11592  fzocatel  11594  fzoend  11610  peano2fzor  11624  monoord2  11829  sermono  11830  expmulnbnd  11988  bcpasc  12089  ccatcl  12266  swrdcl  12307  revcl  12393  revlen  12394  fsum0diag2  13242  isumsplit  13295  sadadd  13655  sadass  13659  smuval2  13670  smumul  13681  vdwapun  14027  vdwlem9  14042  ramub1lem1  14079  prdsbasfn  14401  prdsbasprj  14402  pwsplusgval  14420  pwsmulrval  14421  pwsvscafval  14424  xpsaddlem  14505  xpsvsca  14509  xpsle  14511  mreexmrid  14573  homfeqval  14628  comfval2  14634  comfeq  14637  comfeqval  14639  oppccomfpropd  14658  invco  14701  sectepi  14710  issubc3  14751  funcf2  14770  funciso  14776  fthepi  14830  nat1st2nd  14853  fuciso  14877  homarcl2  14895  coapm  14931  setcmon  14947  setcepi  14948  setcsect  14949  setcinv  14950  setciso  14951  catccatid  14962  resscatc  14965  catciso  14967  catcoppccl  14968  catcfuccl  14969  xpccatid  14990  catcxpccl  15009  xpcpropd  15010  evlfcl  15024  curfpropd  15035  hofcl  15061  yonedalem3  15082  yonffthlem  15084  poslubdg  15311  grpidd  15435  ismndd  15436  mndpropd  15438  issubmnd  15441  submnd0  15443  imasmnd  15451  gsumress  15498  frmdelbas  15522  grpidd2  15566  submmulg  15653  pwsinvg  15658  imasgrp  15662  subginvcl  15681  subgcl  15682  subgsub  15684  subgmulg  15686  divseccl  15728  gaid2  15812  submod  16059  odsubdvds  16061  sylow1lem4  16091  sylow2alem2  16108  lsmdisj2  16170  subgdisj1  16179  pj1id  16187  efgsrel  16222  efgrelexlemb  16238  efgcpbl2  16245  frgpcpbl  16247  frgp0  16248  frgpeccl  16249  frgpadd  16251  frgpup3lem  16265  frgpnabllem1  16342  cycsubgcyg  16368  prdsgsum  16459  prdsgsumOLD  16460  dprdfeq0  16500  dprdfeq0OLD  16507  dmdprdsplitlem  16522  dmdprdsplitlemOLD  16523  dpjidcl  16545  dpjidclOLD  16552  pgpfac1lem3a  16565  pgpfac1lem4  16567  pgpfaclem1  16570  pgpfaclem2  16571  ablfaclem2  16575  rngidss  16659  rngpropd  16664  imasrng  16699  divsrng2  16700  subrg1  16853  subrgmcl  16855  subrgdv  16860  subrgunit  16861  issubdrg  16868  resrhm  16872  lmodprop2d  16985  0lmhm  17098  lmhmpropd  17131  lspfixed  17186  lssacsex  17202  lbsextlem4  17219  divscrng  17299  assapropd  17375  psrelbas  17427  resspsrvsca  17467  subrgpsr  17468  mplcoe1  17521  mplbas2  17526  mplbas2OLD  17527  mplascl  17553  mplmon2cl  17557  mplmon2mul  17558  evlrhm  17586  mpfconst  17591  vr1cl2  17624  ply1lss  17627  ply1subrg  17628  psropprmul  17668  evl1vsd  17753  evl1expd  17754  evl1gsumadd  17767  evl1gsummon  17774  znf1o  17959  psgnghm2  17986  elocv  18068  pjff  18112  frlmlss  18151  frlmsubgval  18167  frlmvscafval  18168  frlmphl  18181  uvcresum  18193  frlmssuvc1  18194  frlmssuvc2  18195  frlmssuvc1OLD  18196  frlmssuvc2OLD  18197  frlmsslsp  18198  frlmsslspOLD  18199  frlmup1  18201  matrng  18305  matassa  18306  mat1  18309  mattposcl  18312  mavmulass  18335  mdetunilem9  18401  matinv  18458  elcls3  18662  mreclatdemoBAD  18675  neiptopnei  18711  resstps  18766  ordtrest2lem  18782  ordtrest2  18783  pnfnei  18799  mnfnei  18800  iscnp2  18818  iscnp4  18842  cnrest2r  18866  lmcls  18881  lmcld  18882  cnt0  18925  cnhaus  18933  isreg2  18956  conclo  18994  1stccnp  19041  loclly  19066  lly1stc  19075  kgencmp2  19094  llycmpkgen2  19098  kgen2ss  19103  kgencn3  19106  pttoponconst  19145  txcls  19152  txbasval  19154  dfac14lem  19165  ptcn  19175  ptrescn  19187  txtube  19188  txcmplem1  19189  txlm  19196  txkgen  19200  xkopjcn  19204  cnmptkp  19228  xkoinjcn  19235  qtopkgen  19258  imastps  19269  isr0  19285  r0cld  19286  pt1hmeo  19354  ptuncnv  19355  ptunhmeo  19356  filintn0  19409  trnei  19440  flimfil  19517  flimopn  19523  fbflim2  19525  cnpflf2  19548  flfcnp  19552  flfcnp2  19555  fclsopn  19562  fcfnei  19583  cnpfcf  19589  alexsublem  19591  ptcmplem3  19601  ptcmplem4  19602  cnextfres  19615  tmdcn2  19635  tmdgsum  19641  tmdgsum2  19642  symgtgp  19647  tgphaus  19662  tgpt1  19663  divstgplem  19666  prdstmdd  19669  prdstgpd  19670  haustsms  19681  tsmscls  19683  tsmsmhm  19695  tsmsadd  19696  tgptsmscls  19699  tsmssplit  19701  restutop  19787  utopreg  19802  ressusp  19815  ucncn  19835  xmetunirn  19887  ressprdsds  19921  xpsdsval  19931  xblss2ps  19951  blbas  19980  mopntopon  19989  isxms2  19998  imasf1oxms  20039  imasf1oms  20040  prdsxmslem2  20079  tmsxpsval  20088  tngngp2  20213  tngngp  20215  tgioo  20348  metdseq0  20405  cncfmpt2f  20465  cncfcnvcn  20472  cnmptre  20474  cnheibor  20502  nmhmcn  20650  cvsdiv  20656  cvsdivcl  20657  cphsubrglem  20671  cphreccllem  20672  iscmet3  20779  relcmpcmet  20802  bcthlem4  20813  rrxds  20872  minveclem4  20894  ivthicc  20917  evthicc  20918  ovolicc2lem4  20978  ovolicc2lem5  20979  iunmbl2  21013  vitalilem3  21065  cncombf  21111  cnmbf  21112  dvres2lem  21360  cpncn  21385  cpnres  21386  dvaddbr  21387  dvmulbr  21388  dvcobr  21395  dvcjbr  21398  dvrec  21404  dvcnvlem  21423  dvlip2  21442  dvivth  21457  lhop2  21462  lhop  21463  dvcnvrelem1  21464  dvcnvrelem2  21465  dvcnvre  21466  ftc1lem6  21488  mdegvscale  21521  mdegvsca  21522  fta1blem  21615  plyaddlem1  21656  plymullem1  21657  coeeulem  21667  tayl0  21802  taylthlem1  21813  taylthlem2  21814  ulmdvlem3  21842  psercnlem2  21864  psercn  21866  cxpcn3  22161  loglesqr  22171  efrlim  22338  ppinprm  22465  chtnprm  22467  dchrptlem1  22578  dchrptlem2  22579  tgbtwnouttr2  22923  tgldim0eq  22931  tgifscgr  22936  ercgrg  22944  tgcgrxfr  22945  tgcolg  22962  tgbtwnconn1lem2  22976  tgbtwnconn1lem3  22977  legtri3  22992  legbtwn  22996  ncolne1  23003  tgisline  23005  tglinethru  23012  colline  23020  mirinv  23036  miriso  23039  mirauto  23043  miduniq  23044  krippenlem  23049  midexlem  23051  f1otrg  23068  axlowdimlem16  23154  elntg  23181  eengtrkg  23182  eengtrkge  23183  eupap1  23548  grpoidinv2  23656  grpoinv  23665  ubthlem2  24223  shuni  24654  fpwrelmap  25984  rngurd  26207  kerf1hrm  26243  ordtrest2NEWlem  26304  ordtrest2NEW  26305  lmxrge0  26334  nmmulg  26349  rrhcn  26378  esumadd  26459  esumaddf  26464  esumcocn  26481  measiuns  26583  mbfmco2  26632  dya2iocnrect  26648  oms0  26662  sibf0  26672  sibfof  26678  fibp1  26736  ccatmulgnn0dir  26892  indispcon  27075  conpcon  27076  pconpi1  27078  sconpi1  27080  cvmsss2  27115  cvmliftmolem1  27122  cvmliftlem8  27133  cvmliftlem10  27135  cvmliftlem11  27136  cvmlift2lem9  27152  cvmlift2lem12  27155  cvmlift3lem7  27166  fprodser  27413  linethru  28135  areacirclem4  28440  ivthALT  28483  locfincmp  28529  comppfsc  28532  neibastop2  28535  filnetlem4  28555  fdc  28594  isbnd3  28636  prdsbnd  28645  prdstotbnd  28646  prdsbnd2  28647  rrnequiv  28687  reheibor  28691  iscringd  28752  isfldidl  28821  diophin  29064  acongeq  29279  isnumbasgrplem2  29413  proot1mul  29517  stoweidlem26  29774  stoweidlem27  29775  stoweidlem31  29779  stoweidlem34  29782  el2fzo  30165  fzoopth  30166  zpnn0elfzo1  30175  ccatw2s1p2  30223  zlmodzxzel  30703  suctrALT  31449  bnj1450  31928  bnj1501  31945  eqlkr  32584  ldualvsubval  32642  dvalveclem  34510  dia2dimlem5  34553  dia2dimlem9  34557  tendoinvcl  34589  dvhgrp  34592  dvhlveclem  34593  dihpN  34821  dochsnkr2cl  34959  lcfl7lem  34984  lclkr  35018  lclkrs  35024  lcfrvalsnN  35026  lcfrlem4  35030  lcfrlem6  35032  lcfrlem16  35043  lcdvsubval  35103  lcdlkreqN  35107  mapdcl2  35141  mapdincl  35146  mapdlsmcl  35148  mapdpglem3  35160  hdmaprnlem9N  35345  hdmaplkr  35401  hdmapip0  35403  hdmapglem7a  35415