Theorem syl5eqelr 2550

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 1819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-ext 2435

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

This theorem is referenced by:  3eltr3g  2561  dmrnssfld  5271  opabbrexOLD  6339  oprssdm  6455  offval  6546  cnvexg  6745  resfunexgALT  6762  abrexexg  6774  abrexex2g  6776  opabex3d  6777  suppssov1  6950  suppssfv  6954  ralxpmap  7487  imafi  7831  abrexfi  7838  ssfii  7897  wdomima2g  8030  unxpwdom2  8032  tskwe  8348  ac10ct  8432  fin23lem28  8737  fin23lem30  8739  axcclem  8854  distrlem4pr  9421  iccshftr  11679  iccshftl  11681  iccdil  11683  icccntr  11685  o1res  13395  exprmfct  14263  infpnlem1  14440  4sqlem13  14487  0ram  14550  ressval3d  14708  ismred2  15020  mreexexlem2d  15062  mreexexlem4d  15064  acsfn1c  15079  acsfn2  15080  ssclem  15235  submacs  16123  efgrcl  16860  dprd2da  17218  srgbinom  17323  irredlmul  17484  lidlrsppropd  18005  issubassa  18100  ply1crng  18364  ply1ring  18416  ply1lmod  18420  chrcl  18690  css1  18848  oftpos  19081  tposmap  19086  0opn  19540  fctop2  19633  difopn  19662  tgrest  19787  ordtbas2  19819  ordtopn3  19824  ordtcld3  19827  t1ficld  19955  resthauslem  19991  kgentopon  20165  txbasex  20193  txcnpi  20235  txdis1cn  20262  pthaus  20265  txkgen  20279  cnmptid  20288  cnmptc  20289  cnmpt1st  20295  cnmpt2nd  20296  cnmpt2c  20297  cnmptkc  20306  txcon  20316  hmeoima  20392  hmeocld  20394  xkohmeo  20442  filufint  20547  fin1aufil  20559  flftg  20623  ptcmplem2  20679  tmdmulg  20717  tmdgsum2  20721  symgtgp  20726  submtmd  20729  ghmcnp  20739  qustgpopn  20744  qustgplem  20745  ust0  20848  nrginvrcn  21326  fsumcn  21500  fsum2cn  21501  expcn  21502  cnheibor  21581  evth2  21586  csscld  21815  clsocv  21816  ovoliun2  22043  volfiniun  22083  dyadmbl  22135  mbfeqalem  22175  mbfss  22179  ismbf3d  22187  mbfadd  22194  i1f0rn  22215  mbfmul  22259  itg2seq  22275  itg2monolem2  22284  itg2monolem3  22285  itg2mono  22286  itgreval  22329  itgge0  22343  itgss3  22347  iblconst  22350  itgconst  22351  ibladdlem  22352  itgfsum  22359  iblabslem  22360  itgabs  22367  mvth  22519  lhop1lem  22540  dvfsumle  22548  dvfsumlem2  22554  ftc1lem4  22566  itgparts  22574  itgsubstlem  22575  itgsubst  22576  plydivlem1  22815  aannenlem1  22850  taylply2  22889  itgulm  22929  cxpcn  23245  resqrtcn  23249  basellem1  23480  mulogsumlem  23842  mulog2sumlem2  23846  selberg2lem  23861  pntrsumo1  23876  nbgracnvfv  24567  zrdivrng  25561  pjssmii  26726  abrexexd  27535  ogrpaddltrbid  27871  pl1cn  28098  esumcvg  28258  esumcvgsum  28260  sigaval  28283  sigaclfu2  28294  measinb2  28367  braew  28387  unelcarsg  28455  carsgclctunlem2  28461  sibfof  28479  sitgclg  28481  orrvcoel  28601  orrvccel  28602  subfaclefac  28817  cvmsss2  28916  cvmopnlem  28920  mpstrcl  29098  elmpps  29130  mblfinlem1  30235  cnambfre  30247  ibladdnclem  30255  iblabsnclem  30262  itgabsnc  30268  ftc1cnnclem  30272  ftc1anclem4  30277  ftc1anclem5  30278  ftc1anclem6  30279  ftc1anclem7  30280  ftc2nc  30283  areacirc  30296  hmeoclda  30335  mzpconstmpt  30856  mzpresrename  30867  diophrex  30893  0dioph  30896  anrabdioph  30898  orrabdioph  30899  rabren3dioph  30932  dvradcnv2  31435  xpexb  31546  fsumcnf  31578  fprodcncf  31886  iblconstmpt  31936  itgiccshift  31961  itgperiod  31962  itgsbtaddcnst  31963  dirkercncflem2  32068  fourierdlem47  32118  aoprssdm  32469  residfi  32557  bj-1uplex  34688  bj-2uplex  34702  bj-diagval  34727  dalemrot  35503  dalem10  35519  arglem1N  36037  cdlemk36  36761