Theorem syl5eqelr 2515

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

Syntax hints:   -> wi 4   = wceq 1437   e. wcel 1868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-cleq 2414  df-clel 2417

This theorem is referenced by:  3eltr3g  2526  dmrnssfld  5108  opabbrexOLD  6344  oprssdm  6460  offval  6548  cnvexg  6749  resfunexgALT  6766  abrexexg  6778  abrexex2g  6780  opabex3d  6781  suppssov1  6954  suppssfv  6958  ralxpmap  7525  imafi  7869  abrexfi  7876  ssfii  7935  wdomima2g  8103  unxpwdom2  8105  tskwe  8385  ac10ct  8465  fin23lem28  8770  fin23lem30  8772  axcclem  8887  distrlem4pr  9451  iccshftr  11766  iccshftl  11768  iccdil  11770  icccntr  11772  o1res  13611  exprmfct  14635  infpnlem1  14841  4sqlem13OLD  14888  4sqlem13  14894  0ram  14965  ressval3d  15173  ismred2  15496  mreexexlem2d  15538  mreexexlem4d  15540  acsfn1c  15555  acsfn2  15556  ssclem  15711  submacs  16599  efgrcl  17352  dprd2da  17662  srgbinom  17765  irredlmul  17923  lidlrsppropd  18441  issubassa  18535  ply1crng  18778  ply1ring  18828  ply1lmod  18832  chrcl  19083  css1  19239  oftpos  19463  tposmap  19468  0opn  19920  fctop2  20006  difopn  20035  tgrest  20161  ordtbas2  20193  ordtopn3  20198  ordtcld3  20201  t1ficld  20329  resthauslem  20365  kgentopon  20539  txbasex  20567  txcnpi  20609  txdis1cn  20636  pthaus  20639  txkgen  20653  cnmptid  20662  cnmptc  20663  cnmpt1st  20669  cnmpt2nd  20670  cnmpt2c  20671  cnmptkc  20680  txcon  20690  hmeoima  20766  hmeocld  20768  xkohmeo  20816  filufint  20921  fin1aufil  20933  flftg  20997  ptcmplem2  21054  tmdmulg  21093  tmdgsum2  21097  symgtgp  21102  submtmd  21105  ghmcnp  21115  qustgpopn  21120  qustgplem  21121  ust0  21220  nrginvrcn  21680  fsumcn  21888  fsum2cn  21889  expcn  21890  cnheibor  21969  evth2  21974  csscld  22206  clsocv  22207  ovoliun2  22445  volfiniun  22486  dyadmbl  22544  mbfeqalem  22584  mbfss  22588  ismbf3d  22596  mbfadd  22603  i1f0rn  22626  mbfmul  22670  itg2seq  22686  itg2monolem2  22695  itg2monolem3  22696  itg2mono  22697  itgreval  22740  itgge0  22754  itgss3  22758  iblconst  22761  itgconst  22762  ibladdlem  22763  itgfsum  22770  iblabslem  22771  itgabs  22778  mvth  22930  lhop1lem  22951  dvfsumle  22959  dvfsumlem2  22965  ftc1lem4  22977  itgparts  22985  itgsubstlem  22986  itgsubst  22987  plydivlem1  23232  aannenlem1  23270  taylply2  23309  itgulm  23349  cxpcn  23671  resqrtcn  23675  basellem1  23993  mulogsumlem  24355  mulog2sumlem2  24359  selberg2lem  24374  pntrsumo1  24389  nbgracnvfv  25153  zrdivrng  26145  pjssmii  27319  abrexexd  28129  ogrpaddltrbid  28478  lmatfval  28635  pl1cn  28756  esumcvg  28902  esumcvgsum  28904  sigaval  28927  sigaclfu2  28938  sigapildsys  28979  ldgenpisys  28983  measinb2  29040  braew  29060  unelcarsg  29139  carsgclctunlem2  29146  sibfof  29168  sitgclg  29170  orrvcoel  29293  orrvccel  29294  subfaclefac  29894  cvmsss2  29992  cvmopnlem  29996  mpstrcl  30174  elmpps  30206  hmeoclda  30981  bj-1uplex  31557  bj-2uplex  31571  bj-diagval  31596  icoreclin  31700  broucube  31887  mblfinlem1  31890  cnambfre  31902  ibladdnclem  31911  iblabsnclem  31918  itgabsnc  31924  ftc1cnnclem  31928  ftc1anclem4  31933  ftc1anclem5  31934  ftc1anclem6  31935  ftc1anclem7  31936  ftc2nc  31939  areacirc  31950  dalemrot  33140  dalem10  33156  arglem1N  33674  cdlemk36  34398  mzpconstmpt  35500  mzpresrename  35510  diophrex  35536  0dioph  35539  anrabdioph  35541  orrabdioph  35542  rabren3dioph  35576  iunrelexp0  36153  dvradcnv2  36553  xpexb  36664  fsumcnf  37202  fprodcncf  37598  iblconstmpt  37651  itgiccshift  37676  itgperiod  37677  itgsbtaddcnst  37678  dirkercncflem2  37785  fourierdlem47  37836  sge0iunmpt  38047  sge0xaddlem2  38063  sge0xadd  38064  aoprssdm  38415  residfi  38727