Theorem syl5eqelr 2489

Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
syl5eqelr.1	|- B = A
syl5eqelr.2	|- ( ph -> B e. C )

Assertion

Ref	Expression
syl5eqelr	|- ( ph -> A e. C )

Proof of Theorem syl5eqelr

Step	Hyp	Ref	Expression
1		syl5eqelr.1	. . 3 |- B = A
2	1	eqcomi 2408	. 2 |- A = B
3		syl5eqelr.2	. 2 |- ( ph -> B e. C )
4	2, 3	syl5eqel 2488	1 |- ( ph -> A e. C )

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

This theorem is referenced by:  dmrnssfld  5088  cnvexg  5364  resfunexgALT  5917  abrexexg  5943  abrexex2g  5947  opabex3d  5948  opabbrex  6077  oprssdm  6187  offval  6271  imafi  7357  abrexfi  7365  ssfii  7382  wdomima2g  7510  unxpwdom2  7512  tskwe  7793  ac10ct  7871  fin23lem28  8176  fin23lem30  8178  axcclem  8293  distrlem4pr  8859  iccshftr  10986  iccshftl  10988  iccdil  10990  icccntr  10992  wrdexb  11718  o1res  12309  exprmfct  13065  infpnlem1  13233  4sqlem13  13280  0ram  13343  ismred2  13783  mreexexlem2d  13825  mreexexlem4d  13827  acsfn1c  13842  acsfn2  13843  ssclem  13974  submacs  14720  efgrcl  15302  dprd2da  15555  irredlmul  15768  lidlrsppropd  16256  issubassa  16338  ply1crng  16551  ply1rng  16597  ply1lmod  16601  chrcl  16762  css1  16872  0opn  16932  fctop2  17024  difopn  17053  tgrest  17177  ordtbas2  17209  ordtopn3  17214  ordtcld3  17217  t1ficld  17345  resthauslem  17381  kgentopon  17523  txbasex  17551  txcnpi  17593  txdis1cn  17620  pthaus  17623  txkgen  17637  cnmptid  17646  cnmptc  17647  cnmpt1st  17653  cnmpt2nd  17654  cnmpt2c  17655  cnmptkc  17664  txcon  17674  hmeoima  17750  hmeocld  17752  xkohmeo  17800  filufint  17905  fin1aufil  17917  flftg  17981  ptcmplem2  18037  tmdmulg  18075  tmdgsum2  18079  symgtgp  18084  submtmd  18087  ghmcnp  18097  divstgpopn  18102  divstgplem  18103  ust0  18202  nrginvrcn  18680  fsumcn  18853  fsum2cn  18854  expcn  18855  cnheibor  18933  evth2  18938  csscld  19156  clsocv  19157  ovoliun2  19355  volfiniun  19394  dyadmbl  19445  mbfeqalem  19487  mbfss  19491  ismbf3d  19499  mbfadd  19506  i1f0rn  19527  mbfmul  19571  itg2seq  19587  itg2monolem2  19596  itg2monolem3  19597  itg2mono  19598  itgreval  19641  itgge0  19655  itgss3  19659  iblconst  19662  itgconst  19663  ibladdlem  19664  itgfsum  19671  iblabslem  19672  itgabs  19679  mvth  19829  lhop1lem  19850  dvfsumle  19858  dvfsumlem2  19864  ftc1lem4  19876  itgparts  19884  itgsubstlem  19885  itgsubst  19886  plydivlem1  20163  aannenlem1  20198  taylply2  20237  itgulm  20277  cxpcn  20582  resqrcn  20586  basellem1  20816  mulogsumlem  21178  mulog2sumlem2  21182  selberg2lem  21197  pntrsumo1  21212  nbgracnvfv  21403  zrdivrng  21973  pjssmii  23136  abrexexd  23943  esumcvg  24429  sigaval  24446  sigaclfu2  24457  measinb2  24530  braew  24546  sibfof  24607  sitgclg  24609  orrvcoel  24676  orrvccel  24677  subfaclefac  24815  cvmsss2  24914  cvmopnlem  24918  mblfinlem  26143  cnambfre  26154  ibladdnclem  26160  iblabsnclem  26167  itgabsnc  26173  ftc1cnnclem  26177  hmeoclda  26226  ralxpmap  26632  mzpconstmpt  26687  mzpresrename  26697  diophrex  26724  0dioph  26727  anrabdioph  26729  orrabdioph  26730  rabren3dioph  26766  xpexb  27525  fsumcnf  27559  aoprssdm  27933  dalemrot  30139  dalem10  30155  arglem1N  30672  cdlemk36  31395

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