Theorem syl5eqelr 2527

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

Syntax hints:   -> wi 4   = wceq 1369   e. wcel 1756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2435  df-clel 2438

This theorem is referenced by:  dmrnssfld  5097  opabbrex  6129  oprssdm  6243  offval  6326  cnvexg  6523  resfunexgALT  6539  abrexexg  6551  abrexex2g  6553  opabex3d  6554  suppssov1  6720  suppssfv  6724  ralxpmap  7261  imafi  7603  abrexfi  7610  ssfii  7668  wdomima2g  7800  unxpwdom2  7802  tskwe  8119  ac10ct  8203  fin23lem28  8508  fin23lem30  8510  axcclem  8625  distrlem4pr  9194  iccshftr  11418  iccshftl  11420  iccdil  11422  icccntr  11424  o1res  13037  exprmfct  13795  infpnlem1  13970  4sqlem13  14017  0ram  14080  ismred2  14540  mreexexlem2d  14582  mreexexlem4d  14584  acsfn1c  14599  acsfn2  14600  ssclem  14731  submacs  15492  efgrcl  16211  dprd2da  16540  srgbinom  16642  irredlmul  16799  lidlrsppropd  17311  issubassa  17394  ply1crng  17653  ply1rng  17702  ply1lmod  17706  chrcl  17956  css1  18114  oftpos  18332  tposmap  18341  0opn  18516  fctop2  18608  difopn  18637  tgrest  18762  ordtbas2  18794  ordtopn3  18799  ordtcld3  18802  t1ficld  18930  resthauslem  18966  kgentopon  19110  txbasex  19138  txcnpi  19180  txdis1cn  19207  pthaus  19210  txkgen  19224  cnmptid  19233  cnmptc  19234  cnmpt1st  19240  cnmpt2nd  19241  cnmpt2c  19242  cnmptkc  19251  txcon  19261  hmeoima  19337  hmeocld  19339  xkohmeo  19387  filufint  19492  fin1aufil  19504  flftg  19568  ptcmplem2  19624  tmdmulg  19662  tmdgsum2  19666  symgtgp  19671  submtmd  19674  ghmcnp  19684  divstgpopn  19689  divstgplem  19690  ust0  19793  nrginvrcn  20271  fsumcn  20445  fsum2cn  20446  expcn  20447  cnheibor  20526  evth2  20531  csscld  20760  clsocv  20761  ovoliun2  20988  volfiniun  21027  dyadmbl  21079  mbfeqalem  21119  mbfss  21123  ismbf3d  21131  mbfadd  21138  i1f0rn  21159  mbfmul  21203  itg2seq  21219  itg2monolem2  21228  itg2monolem3  21229  itg2mono  21230  itgreval  21273  itgge0  21287  itgss3  21291  iblconst  21294  itgconst  21295  ibladdlem  21296  itgfsum  21303  iblabslem  21304  itgabs  21311  mvth  21463  lhop1lem  21484  dvfsumle  21492  dvfsumlem2  21498  ftc1lem4  21510  itgparts  21518  itgsubstlem  21519  itgsubst  21520  plydivlem1  21758  aannenlem1  21793  taylply2  21832  itgulm  21872  cxpcn  22182  resqrcn  22186  basellem1  22417  mulogsumlem  22779  mulog2sumlem2  22783  selberg2lem  22798  pntrsumo1  22813  nbgracnvfv  23348  zrdivrng  23918  pjssmii  25083  abrexexd  25889  ogrpaddltrbid  26183  pl1cn  26384  rrhcn  26425  esumcvg  26534  sigaval  26552  sigaclfu2  26563  measinb2  26636  braew  26657  sibfof  26725  sitgclg  26727  orrvcoel  26847  orrvccel  26848  subfaclefac  27063  cvmsss2  27162  cvmopnlem  27166  mblfinlem1  28426  cnambfre  28438  ibladdnclem  28446  iblabsnclem  28453  itgabsnc  28459  ftc1cnnclem  28463  ftc1anclem4  28468  ftc1anclem5  28469  ftc1anclem6  28470  ftc1anclem7  28471  ftc2nc  28474  areacirc  28487  hmeoclda  28526  mzpconstmpt  29074  mzpresrename  29085  diophrex  29112  0dioph  29115  anrabdioph  29117  orrabdioph  29118  rabren3dioph  29152  xpexb  29708  fsumcnf  29741  aoprssdm  30106  bj-1uplex  32499  bj-2uplex  32513  bj-diagval  32523  dalemrot  33299  dalem10  33315  arglem1N  33832  cdlemk36  34555