Theorem syl5eqelr 2518

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

Syntax hints:   -> wi 4   = wceq 1362   e. wcel 1755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426  df-clel 2429

This theorem is referenced by:  dmrnssfld  5085  opabbrex  6119  oprssdm  6233  offval  6316  cnvexg  6513  resfunexgALT  6529  abrexexg  6541  abrexex2g  6543  opabex3d  6544  suppssov1  6710  suppssfv  6714  ralxpmap  7250  imafi  7592  abrexfi  7599  ssfii  7657  wdomima2g  7789  unxpwdom2  7791  tskwe  8108  ac10ct  8192  fin23lem28  8497  fin23lem30  8499  axcclem  8614  distrlem4pr  9182  iccshftr  11405  iccshftl  11407  iccdil  11409  icccntr  11411  o1res  13021  exprmfct  13778  infpnlem1  13953  4sqlem13  14000  0ram  14063  ismred2  14523  mreexexlem2d  14565  mreexexlem4d  14567  acsfn1c  14582  acsfn2  14583  ssclem  14714  submacs  15474  efgrcl  16191  dprd2da  16514  irredlmul  16733  lidlrsppropd  17233  issubassa  17316  ply1crng  17552  ply1rng  17600  ply1lmod  17604  chrcl  17798  css1  17956  oftpos  18174  tposmap  18183  0opn  18358  fctop2  18450  difopn  18479  tgrest  18604  ordtbas2  18636  ordtopn3  18641  ordtcld3  18644  t1ficld  18772  resthauslem  18808  kgentopon  18952  txbasex  18980  txcnpi  19022  txdis1cn  19049  pthaus  19052  txkgen  19066  cnmptid  19075  cnmptc  19076  cnmpt1st  19082  cnmpt2nd  19083  cnmpt2c  19084  cnmptkc  19093  txcon  19103  hmeoima  19179  hmeocld  19181  xkohmeo  19229  filufint  19334  fin1aufil  19346  flftg  19410  ptcmplem2  19466  tmdmulg  19504  tmdgsum2  19508  symgtgp  19513  submtmd  19516  ghmcnp  19526  divstgpopn  19531  divstgplem  19532  ust0  19635  nrginvrcn  20113  fsumcn  20287  fsum2cn  20288  expcn  20289  cnheibor  20368  evth2  20373  csscld  20602  clsocv  20603  ovoliun2  20830  volfiniun  20869  dyadmbl  20921  mbfeqalem  20961  mbfss  20965  ismbf3d  20973  mbfadd  20980  i1f0rn  21001  mbfmul  21045  itg2seq  21061  itg2monolem2  21070  itg2monolem3  21071  itg2mono  21072  itgreval  21115  itgge0  21129  itgss3  21133  iblconst  21136  itgconst  21137  ibladdlem  21138  itgfsum  21145  iblabslem  21146  itgabs  21153  mvth  21305  lhop1lem  21326  dvfsumle  21334  dvfsumlem2  21340  ftc1lem4  21352  itgparts  21360  itgsubstlem  21361  itgsubst  21362  plydivlem1  21643  aannenlem1  21678  taylply2  21717  itgulm  21757  cxpcn  22067  resqrcn  22071  basellem1  22302  mulogsumlem  22664  mulog2sumlem2  22668  selberg2lem  22683  pntrsumo1  22698  nbgracnvfv  23171  zrdivrng  23741  pjssmii  24906  abrexexd  25713  ogrpaddltrbid  26007  pl1cn  26238  rrhcn  26279  esumcvg  26388  sigaval  26406  sigaclfu2  26417  measinb2  26490  braew  26511  sibfof  26573  sitgclg  26575  orrvcoel  26695  orrvccel  26696  subfaclefac  26911  cvmsss2  27010  cvmopnlem  27014  mblfinlem1  28269  cnambfre  28281  ibladdnclem  28289  iblabsnclem  28296  itgabsnc  28302  ftc1cnnclem  28306  ftc1anclem4  28311  ftc1anclem5  28312  ftc1anclem6  28313  ftc1anclem7  28314  ftc2nc  28317  areacirc  28330  hmeoclda  28369  mzpconstmpt  28918  mzpresrename  28929  diophrex  28956  0dioph  28959  anrabdioph  28961  orrabdioph  28962  rabren3dioph  28996  xpexb  29552  fsumcnf  29585  aoprssdm  29951  bj-1uplex  32081  bj-2uplex  32095  bj-diagval  32102  dalemrot  32871  dalem10  32887  arglem1N  33404  cdlemk36  34127