Theorem eleqtrd 2511

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 1757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-12 1793  ax-ext 2416

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

This theorem is referenced by:  eleqtrrd  2512  3eltr3d  2515  syl5eleq  2521  syl6eleq  2525  opth1  4555  0nelop  4571  fviss  5739  tfisi  6460  fnwelem  6678  omeulem1  7011  oeeulem  7030  oeeui  7031  oaabs2  7074  omabs  7076  ercl  7102  erth  7135  ecelqsdm  7160  ordtypelem6  7727  ordtypelem7  7728  cantnfval  7866  cantnfp1lem3  7878  cantnflem4  7890  cantnfvalOLD  7896  cantnfp1lem3OLD  7904  cantnflem4OLD  7912  r1pwss  7981  rankonidlem  8025  rankxplim3  8078  fseqenlem2  8185  iunfictbso  8274  dfac12lem1  8302  dfac12lem2  8303  fin23lem30  8501  iundom2g  8694  fpwwe2lem6  8792  fpwwe2lem9  8795  lincmb01cmp  11417  fzopth  11484  fzoaddel2  11584  fzosubel2  11586  fzocatel  11588  fzoend  11604  peano2fzor  11618  monoord2  11823  sermono  11824  expmulnbnd  11982  bcpasc  12083  ccatcl  12260  swrdcl  12301  revcl  12387  revlen  12388  fsum0diag2  13235  isumsplit  13288  sadadd  13648  sadass  13652  smuval2  13663  smumul  13674  vdwapun  14020  vdwlem9  14035  ramub1lem1  14072  prdsbasfn  14394  prdsbasprj  14395  pwsplusgval  14413  pwsmulrval  14414  pwsvscafval  14417  xpsaddlem  14498  xpsvsca  14502  xpsle  14504  mreexmrid  14566  homfeqval  14621  comfval2  14627  comfeq  14630  comfeqval  14632  oppccomfpropd  14651  invco  14694  sectepi  14703  issubc3  14744  funcf2  14763  funciso  14769  fthepi  14823  nat1st2nd  14846  fuciso  14870  homarcl2  14888  coapm  14924  setcmon  14940  setcepi  14941  setcsect  14942  setcinv  14943  setciso  14944  catccatid  14955  resscatc  14958  catciso  14960  catcoppccl  14961  catcfuccl  14962  xpccatid  14983  catcxpccl  15002  xpcpropd  15003  evlfcl  15017  curfpropd  15028  hofcl  15054  yonedalem3  15075  yonffthlem  15077  poslubdg  15304  grpidd  15428  ismndd  15429  mndpropd  15431  issubmnd  15434  submnd0  15436  imasmnd  15444  gsumress  15489  frmdelbas  15513  grpidd2  15557  submmulg  15644  pwsinvg  15649  imasgrp  15653  subginvcl  15672  subgcl  15673  subgsub  15675  subgmulg  15677  divseccl  15719  gaid2  15803  submod  16050  odsubdvds  16052  sylow1lem4  16082  sylow2alem2  16099  lsmdisj2  16161  subgdisj1  16170  pj1id  16178  efgsrel  16213  efgrelexlemb  16229  efgcpbl2  16236  frgpcpbl  16238  frgp0  16239  frgpeccl  16240  frgpadd  16242  frgpup3lem  16256  frgpnabllem1  16333  cycsubgcyg  16359  prdsgsum  16447  prdsgsumOLD  16448  dprdfeq0  16488  dprdfeq0OLD  16495  dmdprdsplitlem  16510  dmdprdsplitlemOLD  16511  dpjidcl  16533  dpjidclOLD  16540  pgpfac1lem3a  16553  pgpfac1lem4  16555  pgpfaclem1  16558  pgpfaclem2  16559  ablfaclem2  16563  rngidss  16609  rngpropd  16614  imasrng  16648  divsrng2  16649  subrg1  16801  subrgmcl  16803  subrgdv  16808  subrgunit  16809  issubdrg  16816  resrhm  16820  lmodprop2d  16933  0lmhm  17045  lmhmpropd  17078  lspfixed  17133  lssacsex  17149  lbsextlem4  17166  divscrng  17246  assapropd  17322  psrelbas  17386  resspsrvsca  17426  subrgpsr  17427  mplcoe1  17480  mplbas2  17485  mplbas2OLD  17486  mplascl  17512  mplmon2cl  17516  mplmon2mul  17517  vr1cl2  17550  ply1lss  17553  ply1subrg  17554  psropprmul  17593  znf1o  17828  psgnghm2  17855  elocv  17937  pjff  17981  frlmlss  18020  frlmsubgval  18036  frlmvscafval  18037  frlmphl  18050  uvcresum  18062  frlmssuvc1  18063  frlmssuvc2  18064  frlmssuvc1OLD  18065  frlmssuvc2OLD  18066  frlmsslsp  18067  frlmsslspOLD  18068  frlmup1  18070  matrng  18174  matassa  18175  mat1  18178  mattposcl  18181  mavmulass  18204  mdetunilem9  18270  matinv  18327  elcls3  18531  mreclatdemoBAD  18544  neiptopnei  18580  resstps  18635  ordtrest2lem  18651  ordtrest2  18652  pnfnei  18668  mnfnei  18669  iscnp2  18687  iscnp4  18711  cnrest2r  18735  lmcls  18750  lmcld  18751  cnt0  18794  cnhaus  18802  isreg2  18825  conclo  18863  1stccnp  18910  loclly  18935  lly1stc  18944  kgencmp2  18963  llycmpkgen2  18967  kgen2ss  18972  kgencn3  18975  pttoponconst  19014  txcls  19021  txbasval  19023  dfac14lem  19034  ptcn  19044  ptrescn  19056  txtube  19057  txcmplem1  19058  txlm  19065  txkgen  19069  xkopjcn  19073  cnmptkp  19097  xkoinjcn  19104  qtopkgen  19127  imastps  19138  isr0  19154  r0cld  19155  pt1hmeo  19223  ptuncnv  19224  ptunhmeo  19225  filintn0  19278  trnei  19309  flimfil  19386  flimopn  19392  fbflim2  19394  cnpflf2  19417  flfcnp  19421  flfcnp2  19424  fclsopn  19431  fcfnei  19452  cnpfcf  19458  alexsublem  19460  ptcmplem3  19470  ptcmplem4  19471  cnextfres  19484  tmdcn2  19504  tmdgsum  19510  tmdgsum2  19511  symgtgp  19516  tgphaus  19531  tgpt1  19532  divstgplem  19535  prdstmdd  19538  prdstgpd  19539  haustsms  19550  tsmscls  19552  tsmsmhm  19564  tsmsadd  19565  tgptsmscls  19568  tsmssplit  19570  restutop  19656  utopreg  19671  ressusp  19684  ucncn  19704  xmetunirn  19756  ressprdsds  19790  xpsdsval  19800  xblss2ps  19820  blbas  19849  mopntopon  19858  isxms2  19867  imasf1oxms  19908  imasf1oms  19909  prdsxmslem2  19948  tmsxpsval  19957  tngngp2  20082  tngngp  20084  tgioo  20217  metdseq0  20274  cncfmpt2f  20334  cncfcnvcn  20341  cnmptre  20343  cnheibor  20371  nmhmcn  20519  cvsdiv  20525  cvsdivcl  20526  cphsubrglem  20540  cphreccllem  20541  iscmet3  20648  relcmpcmet  20671  bcthlem4  20682  rrxds  20741  minveclem4  20763  ivthicc  20786  evthicc  20787  ovolicc2lem4  20847  ovolicc2lem5  20848  iunmbl2  20882  vitalilem3  20934  cncombf  20980  cnmbf  20981  dvres2lem  21229  cpncn  21254  cpnres  21255  dvaddbr  21256  dvmulbr  21257  dvcobr  21264  dvcjbr  21267  dvrec  21273  dvcnvlem  21292  dvlip2  21311  dvivth  21326  lhop2  21331  lhop  21332  dvcnvrelem1  21333  dvcnvrelem2  21334  dvcnvre  21335  ftc1lem6  21357  evlrhm  21379  evl1vsd  21390  evl1expd  21391  mpfconst  21392  mdegvscale  21433  mdegvsca  21434  fta1blem  21527  plyaddlem1  21568  plymullem1  21569  coeeulem  21579  tayl0  21714  taylthlem1  21725  taylthlem2  21726  ulmdvlem3  21754  psercnlem2  21776  psercn  21778  cxpcn3  22073  loglesqr  22083  efrlim  22250  ppinprm  22377  chtnprm  22379  dchrptlem1  22490  dchrptlem2  22491  tgbtwnouttr2  22832  tgldim0eq  22840  tgifscgr  22844  ercgrg  22852  tgcgrxfr  22853  tgcolg  22869  tgbtwnconn1lem2  22883  tgbtwnconn1lem3  22884  legtri3  22899  tgisline  22908  tglinethru  22915  colline  22920  miriso  22937  f1otrg  22942  axlowdimlem16  23028  elntg  23055  eengtrkg  23056  eengtrkge  23057  eupap1  23422  grpoidinv2  23530  grpoinv  23539  ubthlem2  24097  shuni  24528  fpwrelmap  25860  rngurd  26111  kerf1hrm  26147  ordtrest2NEWlem  26208  ordtrest2NEW  26209  lmxrge0  26238  nmmulg  26253  rrhcn  26282  esumadd  26363  esumaddf  26368  esumcocn  26385  measiuns  26487  mbfmco2  26536  dya2iocnrect  26552  sibf0  26570  sibfof  26576  fibp1  26634  ccatmulgnn0dir  26790  indispcon  26973  conpcon  26974  pconpi1  26976  sconpi1  26978  cvmsss2  27013  cvmliftmolem1  27020  cvmliftlem8  27031  cvmliftlem10  27033  cvmliftlem11  27034  cvmlift2lem9  27050  cvmlift2lem12  27053  cvmlift3lem7  27064  fprodser  27311  linethru  28033  areacirclem4  28333  ivthALT  28376  locfincmp  28422  comppfsc  28425  neibastop2  28428  filnetlem4  28448  fdc  28487  isbnd3  28529  prdsbnd  28538  prdstotbnd  28539  prdsbnd2  28540  rrnequiv  28580  reheibor  28584  iscringd  28645  isfldidl  28714  diophin  28958  acongeq  29173  isnumbasgrplem2  29307  proot1mul  29411  stoweidlem26  29669  stoweidlem27  29670  stoweidlem31  29674  stoweidlem34  29677  el2fzo  30060  fzoopth  30061  zpnn0elfzo1  30070  ccatw2s1p2  30118  zlmodzxzel  30589  suctrALT  31304  bnj1450  31783  bnj1501  31800  eqlkr  32357  ldualvsubval  32415  dvalveclem  34283  dia2dimlem5  34326  dia2dimlem9  34330  tendoinvcl  34362  dvhgrp  34365  dvhlveclem  34366  dihpN  34594  dochsnkr2cl  34732  lcfl7lem  34757  lclkr  34791  lclkrs  34797  lcfrvalsnN  34799  lcfrlem4  34803  lcfrlem6  34805  lcfrlem16  34816  lcdvsubval  34876  lcdlkreqN  34880  mapdcl2  34914  mapdincl  34919  mapdlsmcl  34921  mapdpglem3  34933  hdmaprnlem9N  35118  hdmaplkr  35174  hdmapip0  35176  hdmapglem7a  35188