Theorem eleqtrd 2480

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

Syntax hints:   -> wi 4   = wceq 1649   e. wcel 1721

This theorem is referenced by:  eleqtrrd  2481  3eltr3d  2484  syl5eleq  2490  syl6eleq  2494  opth1  4394  0nelop  4406  tfisi  4797  fviss  5743  fnwelem  6420  omeulem1  6784  oeeulem  6803  oeeui  6804  oaabs2  6847  omabs  6849  ercl  6875  erth  6908  ecelqsdm  6933  ordtypelem6  7448  ordtypelem7  7449  cantnfval  7579  cantnfp1lem3  7592  cantnflem4  7604  r1pwss  7666  rankonidlem  7710  rankxplim3  7761  fseqenlem2  7862  iunfictbso  7951  dfac12lem1  7979  dfac12lem2  7980  fin23lem30  8178  iundom2g  8371  fpwwe2lem6  8466  fpwwe2lem9  8469  lincmb01cmp  10994  fzopth  11045  fzoaddel2  11131  fzosubel2  11133  fzoend  11142  peano2fzor  11149  monoord2  11309  sermono  11310  expmulnbnd  11466  bcpasc  11567  ccatcl  11698  swrdcl  11721  revcl  11748  revlen  11749  fsum0diag2  12521  isumsplit  12575  sadadd  12934  sadass  12938  smuval2  12949  smumul  12960  vdwapun  13297  vdwlem9  13312  ramub1lem1  13349  prdsbasfn  13648  prdsbasprj  13649  pwsplusgval  13667  pwsmulrval  13668  pwsvscafval  13671  xpsaddlem  13755  xpsvsca  13759  xpsle  13761  mreexmrid  13823  homfeqval  13878  comfval2  13884  comfeq  13887  comfeqval  13889  oppccomfpropd  13908  invco  13951  sectepi  13960  issubc3  14001  funcf2  14020  funciso  14026  fthepi  14080  nat1st2nd  14103  fuciso  14127  homarcl2  14145  coapm  14181  setcmon  14197  setcepi  14198  setcsect  14199  setcinv  14200  setciso  14201  catccatid  14212  resscatc  14215  catciso  14217  catcoppccl  14218  catcfuccl  14219  xpccatid  14240  catcxpccl  14259  xpcpropd  14260  evlfcl  14274  curfpropd  14285  hofcl  14311  yonedalem3  14332  yonffthlem  14334  poslubdg  14530  grpidd  14673  ismndd  14674  mndpropd  14676  issubmnd  14679  submnd0  14680  imasmnd  14688  gsumress  14732  frmdelbas  14753  grpidd2  14797  submmulg  14880  pwsinvg  14885  imasgrp  14889  subginvcl  14908  subgcl  14909  subgsub  14911  subgmulg  14913  divseccl  14951  gaid2  15035  submod  15158  odsubdvds  15160  sylow1lem4  15190  sylow2alem2  15207  lsmdisj2  15269  subgdisj1  15278  pj1id  15286  efgsrel  15321  efgrelexlemb  15337  efgcpbl2  15344  frgpcpbl  15346  frgp0  15347  frgpeccl  15348  frgpadd  15350  frgpup3lem  15364  frgpnabllem1  15439  cycsubgcyg  15465  prdsgsum  15507  dprdfeq0  15535  dmdprdsplitlem  15550  dpjidcl  15571  pgpfac1lem3a  15589  pgpfac1lem4  15591  pgpfaclem1  15594  pgpfaclem2  15595  ablfaclem2  15599  rngidss  15645  rngpropd  15650  imasrng  15680  divsrng2  15681  subrg1  15833  subrgmcl  15835  subrgdv  15840  subrgunit  15841  issubdrg  15848  resrhm  15852  lmodprop2d  15961  0lmhm  16071  lmhmpropd  16100  lspfixed  16155  lssacsex  16171  lbsextlem4  16188  divscrng  16266  assapropd  16341  psrelbas  16399  resspsrvsca  16436  subrgpsr  16437  mplcoe1  16483  mplbas2  16486  mplascl  16511  mplmon2cl  16515  mplmon2mul  16516  vr1cl2  16546  ply1lss  16549  ply1subrg  16550  psropprmul  16587  znf1o  16787  elocv  16850  pjff  16894  elcls3  17102  mreclatdemo  17115  neiptopnei  17151  resstps  17205  ordtrest2lem  17221  ordtrest2  17222  pnfnei  17238  mnfnei  17239  iscnp2  17257  iscnp4  17281  cnrest2r  17305  lmcls  17320  lmcld  17321  cnt0  17364  cnhaus  17372  isreg2  17395  conclo  17431  1stccnp  17478  loclly  17503  lly1stc  17512  kgencmp2  17531  llycmpkgen2  17535  kgen2ss  17540  kgencn3  17543  pttoponconst  17582  txcls  17589  txbasval  17591  dfac14lem  17602  ptcn  17612  ptrescn  17624  txtube  17625  txcmplem1  17626  txlm  17633  txkgen  17637  xkopjcn  17641  cnmptkp  17665  xkoinjcn  17672  qtopkgen  17695  imastps  17706  isr0  17722  r0cld  17723  pt1hmeo  17791  ptuncnv  17792  ptunhmeo  17793  filintn0  17846  trnei  17877  flimfil  17954  flimopn  17960  fbflim2  17962  cnpflf2  17985  flfcnp  17989  flfcnp2  17992  fclsopn  17999  fcfnei  18020  cnpfcf  18026  alexsublem  18028  ptcmplem3  18038  ptcmplem4  18039  cnextfres  18052  tmdcn2  18072  tmdgsum  18078  tmdgsum2  18079  symgtgp  18084  tgphaus  18099  tgpt1  18100  divstgplem  18103  prdstmdd  18106  prdstgpd  18107  haustsms  18118  tsmscls  18120  tsmsmhm  18128  tsmsadd  18129  tgptsmscls  18132  tsmssplit  18134  restutop  18220  utopreg  18235  ressusp  18248  ucncn  18268  xmetunirn  18320  ressprdsds  18354  xpsdsval  18364  xblss2ps  18384  blbas  18413  mopntopon  18422  isxms2  18431  imasf1oxms  18472  imasf1oms  18473  prdsxmslem2  18512  tmsxpsval  18521  tngngp2  18646  tngngp  18648  tgioo  18780  metdseq0  18837  cncfmpt2f  18897  cncfcnvcn  18904  cnmptre  18905  cnheibor  18933  nmhmcn  19081  cphsubrglem  19093  cphreccllem  19094  iscmet3  19199  relcmpcmet  19222  bcthlem4  19233  minveclem4  19286  ivthicc  19308  evthicc  19309  ovolicc2lem4  19369  ovolicc2lem5  19370  iunmbl2  19404  vitalilem3  19455  cncombf  19503  cnmbf  19504  dvres2lem  19750  cpncn  19775  cpnres  19776  dvaddbr  19777  dvmulbr  19778  dvcobr  19785  dvcjbr  19788  dvrec  19794  dvcnvlem  19813  dvlip2  19832  dvivth  19847  lhop2  19852  lhop  19853  dvcnvrelem1  19854  dvcnvrelem2  19855  dvcnvre  19856  ftc1lem6  19878  evlrhm  19899  evl1vsd  19910  evl1expd  19911  mpfconst  19912  mdegvscale  19951  mdegvsca  19952  fta1blem  20044  plyaddlem1  20085  plymullem1  20086  coeeulem  20096  tayl0  20231  taylthlem1  20242  taylthlem2  20243  ulmdvlem3  20271  psercnlem2  20293  psercn  20295  cxpcn3  20585  loglesqr  20595  efrlim  20761  ppinprm  20888  chtnprm  20890  dchrptlem1  21001  dchrptlem2  21002  eupap1  21651  grpoidinv2  21759  grpoinv  21768  ubthlem2  22326  shuni  22755  kerf1hrm  24215  lmxrge0  24290  nmmulg  24305  rrhcn  24333  esumadd  24401  esumaddf  24406  esumcocn  24423  measiuns  24524  mbfmco2  24568  dya2iocnrect  24584  sibf0  24602  sibfof  24607  indispcon  24874  conpcon  24875  pconpi1  24877  sconpi1  24879  cvmsss2  24914  cvmliftmolem1  24921  cvmliftlem8  24932  cvmliftlem10  24934  cvmliftlem11  24935  cvmlift2lem9  24951  cvmlift2lem12  24954  cvmlift3lem7  24965  fprodser  25228  axlowdimlem16  25800  linethru  25991  areacirclem5  26185  ivthALT  26228  locfincmp  26274  comppfsc  26277  neibastop2  26280  filnetlem4  26300  fdc  26339  isbnd3  26383  prdsbnd  26392  prdstotbnd  26393  prdsbnd2  26394  rrnequiv  26434  reheibor  26438  iscringd  26499  isfldidl  26568  diophin  26721  acongeq  26938  frlmlss  27087  frlmvscafval  27098  uvcresum  27110  frlmssuvc1  27114  frlmssuvc2  27115  frlmsslsp  27116  frlmup1  27118  isnumbasgrplem2  27137  psgnghm2  27306  matrng  27348  matassa  27349  mat1  27350  proot1mul  27383  stoweidlem26  27642  stoweidlem27  27643  stoweidlem31  27647  stoweidlem34  27650  bnj1450  29125  bnj1501  29142  eqlkr  29582  ldualvsubval  29640  dvalveclem  31508  dia2dimlem5  31551  dia2dimlem9  31555  tendoinvcl  31587  dvhgrp  31590  dvhlveclem  31591  dihpN  31819  dochsnkr2cl  31957  lcfl7lem  31982  lclkr  32016  lclkrs  32022  lcfrvalsnN  32024  lcfrlem4  32028  lcfrlem6  32030  lcfrlem16  32041  lcdvsubval  32101  lcdlkreqN  32105  mapdcl2  32139  mapdincl  32144  mapdlsmcl  32146  mapdpglem3  32158  hdmaprnlem9N  32343  hdmaplkr  32399  hdmapip0  32401  hdmapglem7a  32413

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400