Theorem eleqtrd 2544

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

Syntax hints:   -> wi 4   = wceq 1370   e. wcel 1758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-cleq 2446  df-clel 2449

This theorem is referenced by:  eleqtrrd  2545  syl5eleq  2548  syl6eleq  2552  3eltr3d  2556  opth1  4676  0nelop  4692  fviss  5861  tfisi  6582  fnwelem  6800  omeulem1  7134  oeeulem  7153  oeeui  7154  oaabs2  7197  omabs  7199  ercl  7225  erth  7258  ecelqsdm  7283  ordtypelem6  7851  ordtypelem7  7852  cantnfval  7990  cantnfp1lem3  8002  cantnflem4  8014  cantnfvalOLD  8020  cantnfp1lem3OLD  8028  cantnflem4OLD  8036  r1pwss  8105  rankonidlem  8149  rankxplim3  8202  fseqenlem2  8309  iunfictbso  8398  dfac12lem1  8426  dfac12lem2  8427  fin23lem30  8625  iundom2g  8818  fpwwe2lem6  8916  fpwwe2lem9  8919  lincmb01cmp  11548  fzopth  11615  fzoaddel2  11718  fzosubel2  11720  fzocatel  11722  fzoend  11738  peano2fzor  11752  monoord2  11957  sermono  11958  expmulnbnd  12116  bcpasc  12217  ccatcl  12395  swrdcl  12436  revcl  12522  revlen  12523  fsum0diag2  13371  isumsplit  13424  sadadd  13784  sadass  13788  smuval2  13799  smumul  13810  vdwapun  14156  vdwlem9  14171  ramub1lem1  14208  prdsbasfn  14531  prdsbasprj  14532  pwsplusgval  14550  pwsmulrval  14551  pwsvscafval  14554  xpsaddlem  14635  xpsvsca  14639  xpsle  14641  mreexmrid  14703  homfeqval  14758  comfval2  14764  comfeq  14767  comfeqval  14769  oppccomfpropd  14788  invco  14831  sectepi  14840  issubc3  14881  funcf2  14900  funciso  14906  fthepi  14960  nat1st2nd  14983  fuciso  15007  homarcl2  15025  coapm  15061  setcmon  15077  setcepi  15078  setcsect  15079  setcinv  15080  setciso  15081  catccatid  15092  resscatc  15095  catciso  15097  catcoppccl  15098  catcfuccl  15099  xpccatid  15120  catcxpccl  15139  xpcpropd  15140  evlfcl  15154  curfpropd  15165  hofcl  15191  yonedalem3  15212  yonffthlem  15214  poslubdg  15441  grpidd  15565  ismndd  15566  mndpropd  15568  issubmnd  15571  submnd0  15573  imasmnd  15581  gsumress  15629  frmdelbas  15653  grpidd2  15697  submmulg  15784  pwsinvg  15789  imasgrp  15793  subginvcl  15812  subgcl  15813  subgsub  15815  subgmulg  15817  divseccl  15859  gaid2  15943  submod  16192  odsubdvds  16194  sylow1lem4  16224  sylow2alem2  16241  lsmdisj2  16303  subgdisj1  16312  pj1id  16320  efgsrel  16355  efgrelexlemb  16371  efgcpbl2  16378  frgpcpbl  16380  frgp0  16381  frgpeccl  16382  frgpadd  16384  frgpup3lem  16398  frgpnabllem1  16475  cycsubgcyg  16501  prdsgsum  16596  prdsgsumOLD  16597  dprdfeq0  16637  dprdfeq0OLD  16644  dmdprdsplitlem  16659  dmdprdsplitlemOLD  16660  dpjidcl  16682  dpjidclOLD  16689  pgpfac1lem3a  16702  pgpfac1lem4  16704  pgpfaclem1  16707  pgpfaclem2  16708  ablfaclem2  16712  rngidss  16797  rngpropd  16802  imasrng  16837  divsrng2  16838  kerf1hrm  16957  subrg1  17001  subrgmcl  17003  subrgdv  17008  subrgunit  17009  issubdrg  17016  resrhm  17020  lmodprop2d  17133  0lmhm  17247  lmhmpropd  17280  lspfixed  17335  lssacsex  17351  lbsextlem4  17368  divscrng  17448  assapropd  17524  psrelbas  17576  resspsrvsca  17617  subrgpsr  17618  mplcoe1  17671  mplbas2  17678  mplbas2OLD  17679  mplascl  17705  mplmon2cl  17709  mplmon2mul  17710  evlrhm  17738  mpfconst  17743  vr1cl2  17776  ply1lss  17779  ply1subrg  17780  psropprmul  17819  evl1vsd  17906  evl1expd  17907  evl1gsumadd  17920  evl1gsummon  17927  znf1o  18112  psgnghm2  18139  elocv  18221  pjff  18265  frlmlss  18304  frlmsubgval  18320  frlmvscafval  18321  frlmphl  18334  uvcresum  18346  frlmssuvc1  18347  frlmssuvc2  18348  frlmssuvc1OLD  18349  frlmssuvc2OLD  18350  frlmsslsp  18351  frlmsslspOLD  18352  frlmup1  18354  matrng  18459  matassa  18460  mat1  18464  mattposcl  18467  mavmulass  18490  mdetunilem9  18561  matinv  18618  elcls3  18822  mreclatdemoBAD  18835  neiptopnei  18871  resstps  18926  ordtrest2lem  18942  ordtrest2  18943  pnfnei  18959  mnfnei  18960  iscnp2  18978  iscnp4  19002  cnrest2r  19026  lmcls  19041  lmcld  19042  cnt0  19085  cnhaus  19093  isreg2  19116  conclo  19154  1stccnp  19201  loclly  19226  lly1stc  19235  kgencmp2  19254  llycmpkgen2  19258  kgen2ss  19263  kgencn3  19266  pttoponconst  19305  txcls  19312  txbasval  19314  dfac14lem  19325  ptcn  19335  ptrescn  19347  txtube  19348  txcmplem1  19349  txlm  19356  txkgen  19360  xkopjcn  19364  cnmptkp  19388  xkoinjcn  19395  qtopkgen  19418  imastps  19429  isr0  19445  r0cld  19446  pt1hmeo  19514  ptuncnv  19515  ptunhmeo  19516  filintn0  19569  trnei  19600  flimfil  19677  flimopn  19683  fbflim2  19685  cnpflf2  19708  flfcnp  19712  flfcnp2  19715  fclsopn  19722  fcfnei  19743  cnpfcf  19749  alexsublem  19751  ptcmplem3  19761  ptcmplem4  19762  cnextfres  19775  tmdcn2  19795  tmdgsum  19801  tmdgsum2  19802  symgtgp  19807  tgphaus  19822  tgpt1  19823  divstgplem  19826  prdstmdd  19829  prdstgpd  19830  haustsms  19841  tsmscls  19843  tsmsmhm  19855  tsmsadd  19856  tgptsmscls  19859  tsmssplit  19861  restutop  19947  utopreg  19962  ressusp  19975  ucncn  19995  xmetunirn  20047  ressprdsds  20081  xpsdsval  20091  xblss2ps  20111  blbas  20140  mopntopon  20149  isxms2  20158  imasf1oxms  20199  imasf1oms  20200  prdsxmslem2  20239  tmsxpsval  20248  tngngp2  20373  tngngp  20375  tgioo  20508  metdseq0  20565  cncfmpt2f  20625  cncfcnvcn  20632  cnmptre  20634  cnheibor  20662  nmhmcn  20810  cvsdiv  20816  cvsdivcl  20817  cphsubrglem  20831  cphreccllem  20832  iscmet3  20939  relcmpcmet  20962  bcthlem4  20973  rrxds  21032  minveclem4  21054  ivthicc  21077  evthicc  21078  ovolicc2lem4  21138  ovolicc2lem5  21139  iunmbl2  21174  vitalilem3  21226  cncombf  21272  cnmbf  21273  dvres2lem  21521  cpncn  21546  cpnres  21547  dvaddbr  21548  dvmulbr  21549  dvcobr  21556  dvcjbr  21559  dvrec  21565  dvcnvlem  21584  dvlip2  21603  dvivth  21618  lhop2  21623  lhop  21624  dvcnvrelem1  21625  dvcnvrelem2  21626  dvcnvre  21627  ftc1lem6  21649  mdegvscale  21682  mdegvsca  21683  fta1blem  21776  plyaddlem1  21817  plymullem1  21818  coeeulem  21828  tayl0  21963  taylthlem1  21974  taylthlem2  21975  ulmdvlem3  22003  psercnlem2  22025  psercn  22027  cxpcn3  22322  loglesqr  22332  efrlim  22499  ppinprm  22626  chtnprm  22628  dchrptlem1  22739  dchrptlem2  22740  tgbtwnouttr2  23086  tgldim0eq  23094  tgifscgr  23100  ercgrg  23108  tgcgrxfr  23109  tgcolg  23127  tgbtwnconn1lem2  23145  tgbtwnconn1lem3  23146  legtri3  23162  legbtwn  23166  ncolne1  23173  tgisline  23175  tglinethru  23184  coltr3  23196  colline  23197  tglowdim2ln  23199  mirinv  23214  miriso  23217  mirauto  23222  miduniq  23223  krippenlem  23228  midexlem  23230  ragperp  23254  footex  23255  colperpexlem1  23259  colperpexlem3  23261  mideulem  23263  mideu  23264  f1otrg  23289  axlowdimlem16  23375  elntg  23402  eengtrkg  23403  eengtrkge  23404  eupap1  23769  grpoidinv2  23877  grpoinv  23886  ubthlem2  24444  shuni  24875  fpwrelmap  26204  rngurd  26421  ordtrest2NEWlem  26517  ordtrest2NEW  26518  lmxrge0  26547  nmmulg  26562  rrhcn  26591  esumadd  26672  esumaddf  26677  esumcocn  26694  measiuns  26796  mbfmco2  26844  dya2iocnrect  26860  oms0  26874  sibf0  26884  sibfof  26890  fibp1  26948  ccatmulgnn0dir  27104  indispcon  27287  conpcon  27288  pconpi1  27290  sconpi1  27292  cvmsss2  27327  cvmliftmolem1  27334  cvmliftlem8  27345  cvmliftlem10  27347  cvmliftlem11  27348  cvmlift2lem9  27364  cvmlift2lem12  27367  cvmlift3lem7  27378  fprodser  27626  linethru  28348  areacirclem4  28655  ivthALT  28698  locfincmp  28744  comppfsc  28747  neibastop2  28750  filnetlem4  28770  fdc  28809  isbnd3  28851  prdsbnd  28860  prdstotbnd  28861  prdsbnd2  28862  rrnequiv  28902  reheibor  28906  iscringd  28967  isfldidl  29036  diophin  29279  acongeq  29494  isnumbasgrplem2  29628  proot1mul  29732  stoweidlem26  29989  stoweidlem27  29990  stoweidlem31  29994  stoweidlem34  29997  el2fzo  30380  fzoopth  30381  zpnn0elfzo1  30390  ccatw2s1p2  30438  zlmodzxzel  30920  ply1mulgsum  31022  cpmadugsumlemF  31382  cpmadugsumfi  31383  cpmidgsum2  31385  suctrALT  31914  bnj1450  32393  bnj1501  32410  eqlkr  33102  ldualvsubval  33160  dvalveclem  35028  dia2dimlem5  35071  dia2dimlem9  35075  tendoinvcl  35107  dvhgrp  35110  dvhlveclem  35111  dihpN  35339  dochsnkr2cl  35477  lcfl7lem  35502  lclkr  35536  lclkrs  35542  lcfrvalsnN  35544  lcfrlem4  35548  lcfrlem6  35550  lcfrlem16  35561  lcdvsubval  35621  lcdlkreqN  35625  mapdcl2  35659  mapdincl  35664  mapdlsmcl  35666  mapdpglem3  35678  hdmaprnlem9N  35863  hdmaplkr  35919  hdmapip0  35921  hdmapglem7a  35933