Theorem syl5eqelr 2560

Description: A 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 2480	. 2 |- A = B
3		syl5eqelr.2	. 2 |- ( ph -> B e. C )
4	2, 3	syl5eqel 2559	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1379   e. wcel 1767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462

This theorem is referenced by:  3eltr3g  2571  dmrnssfld  5261  opabbrex  6324  oprssdm  6440  offval  6531  cnvexg  6730  resfunexgALT  6747  abrexexg  6759  abrexex2g  6761  opabex3d  6762  suppssov1  6932  suppssfv  6936  ralxpmap  7468  imafi  7813  abrexfi  7820  ssfii  7879  wdomima2g  8012  unxpwdom2  8014  tskwe  8331  ac10ct  8415  fin23lem28  8720  fin23lem30  8722  axcclem  8837  distrlem4pr  9404  iccshftr  11654  iccshftl  11656  iccdil  11658  icccntr  11660  o1res  13346  exprmfct  14110  infpnlem1  14287  4sqlem13  14334  0ram  14397  ismred2  14858  mreexexlem2d  14900  mreexexlem4d  14902  acsfn1c  14917  acsfn2  14918  ssclem  15049  submacs  15815  efgrcl  16539  dprd2da  16893  srgbinom  16998  irredlmul  17158  lidlrsppropd  17677  issubassa  17772  ply1crng  18036  ply1rng  18088  ply1lmod  18092  chrcl  18358  css1  18516  oftpos  18749  tposmap  18754  0opn  19208  fctop2  19300  difopn  19329  tgrest  19454  ordtbas2  19486  ordtopn3  19491  ordtcld3  19494  t1ficld  19622  resthauslem  19658  kgentopon  19802  txbasex  19830  txcnpi  19872  txdis1cn  19899  pthaus  19902  txkgen  19916  cnmptid  19925  cnmptc  19926  cnmpt1st  19932  cnmpt2nd  19933  cnmpt2c  19934  cnmptkc  19943  txcon  19953  hmeoima  20029  hmeocld  20031  xkohmeo  20079  filufint  20184  fin1aufil  20196  flftg  20260  ptcmplem2  20316  tmdmulg  20354  tmdgsum2  20358  symgtgp  20363  submtmd  20366  ghmcnp  20376  divstgpopn  20381  divstgplem  20382  ust0  20485  nrginvrcn  20963  fsumcn  21137  fsum2cn  21138  expcn  21139  cnheibor  21218  evth2  21223  csscld  21452  clsocv  21453  ovoliun2  21680  volfiniun  21720  dyadmbl  21772  mbfeqalem  21812  mbfss  21816  ismbf3d  21824  mbfadd  21831  i1f0rn  21852  mbfmul  21896  itg2seq  21912  itg2monolem2  21921  itg2monolem3  21922  itg2mono  21923  itgreval  21966  itgge0  21980  itgss3  21984  iblconst  21987  itgconst  21988  ibladdlem  21989  itgfsum  21996  iblabslem  21997  itgabs  22004  mvth  22156  lhop1lem  22177  dvfsumle  22185  dvfsumlem2  22191  ftc1lem4  22203  itgparts  22211  itgsubstlem  22212  itgsubst  22213  plydivlem1  22451  aannenlem1  22486  taylply2  22525  itgulm  22565  cxpcn  22875  resqrtcn  22879  basellem1  23110  mulogsumlem  23472  mulog2sumlem2  23476  selberg2lem  23491  pntrsumo1  23506  nbgracnvfv  24144  zrdivrng  25138  pjssmii  26303  abrexexd  27109  ogrpaddltrbid  27401  pl1cn  27601  rrhcn  27642  esumcvg  27760  sigaval  27778  sigaclfu2  27789  measinb2  27862  braew  27882  sibfof  27950  sitgclg  27952  orrvcoel  28072  orrvccel  28073  subfaclefac  28288  cvmsss2  28387  cvmopnlem  28391  mblfinlem1  29656  cnambfre  29668  ibladdnclem  29676  iblabsnclem  29683  itgabsnc  29689  ftc1cnnclem  29693  ftc1anclem4  29698  ftc1anclem5  29699  ftc1anclem6  29700  ftc1anclem7  29701  ftc2nc  29704  areacirc  29717  hmeoclda  29756  mzpconstmpt  30304  mzpresrename  30315  diophrex  30341  0dioph  30344  anrabdioph  30346  orrabdioph  30347  rabren3dioph  30381  xpexb  30969  fsumcnf  31002  iblconstmpt  31301  aoprssdm  31782  residfi  31809  bj-1uplex  33665  bj-2uplex  33679  bj-diagval  33695  dalemrot  34471  dalem10  34487  arglem1N  35004  cdlemk36  35727