MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5eqelr Unicode version

Theorem syl5eqelr 2368
Description: B 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
StepHypRef Expression
1 syl5eqelr.1 . . 3  |-  B  =  A
21eqcomi 2287 . 2  |-  A  =  B
3 syl5eqelr.2 . 2  |-  ( ph  ->  B  e.  C )
42, 3syl5eqel 2367 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684
This theorem is referenced by:  dmrnssfld  4938  cnvexg  5208  resfunexgALT  5738  abrexexg  5764  abrexex2g  5768  oprssdm  6002  offval  6085  imafi  7148  abrexfi  7156  ssfii  7172  wdomima2g  7300  unxpwdom2  7302  tskwe  7583  ac10ct  7661  fin23lem28  7966  fin23lem30  7968  axcclem  8083  distrlem4pr  8650  iccshftr  10769  iccshftl  10771  iccdil  10773  icccntr  10775  wrdexb  11449  o1res  12034  exprmfct  12789  infpnlem1  12957  4sqlem13  13004  0ram  13067  ismred2  13505  mreexexlem2d  13547  mreexexlem4d  13549  acsfn1c  13564  acsfn2  13565  ssclem  13696  submacs  14442  efgrcl  15024  dprd2da  15277  irredlmul  15490  lidlrsppropd  15982  issubassa  16064  ply1crng  16277  ply1rng  16326  ply1lmod  16330  chrcl  16480  css1  16590  0opn  16650  fctop2  16742  difopn  16771  tgrest  16890  ordtbas2  16921  ordtopn3  16926  ordtcld3  16929  t1ficld  17055  resthauslem  17091  kgentopon  17233  txbasex  17261  txcnpi  17302  txdis1cn  17329  pthaus  17332  txkgen  17346  cnmptid  17355  cnmptc  17356  cnmpt1st  17362  cnmpt2nd  17363  cnmpt2c  17364  cnmptkc  17373  txcon  17383  hmeoima  17456  hmeocld  17458  xkohmeo  17506  filufint  17615  fin1aufil  17627  flftg  17691  ptcmplem2  17747  tmdmulg  17775  tmdgsum2  17779  symgtgp  17784  submtmd  17787  ghmcnp  17797  divstgpopn  17802  divstgplem  17803  nrginvrcn  18202  fsumcn  18374  fsum2cn  18375  expcn  18376  cnheibor  18453  evth2  18458  csscld  18676  clsocv  18677  ovoliun2  18865  volfiniun  18904  dyadmbl  18955  mbfeqalem  18997  mbfss  19001  ismbf3d  19009  mbfadd  19016  i1f0rn  19037  mbfmul  19081  itg2seq  19097  itg2monolem2  19106  itg2monolem3  19107  itg2mono  19108  itgreval  19151  itgge0  19165  itgss3  19169  iblconst  19172  itgconst  19173  ibladdlem  19174  itgfsum  19181  iblabslem  19182  itgabs  19189  mvth  19339  lhop1lem  19360  dvfsumle  19368  dvfsumlem2  19374  ftc1lem4  19386  itgparts  19394  itgsubstlem  19395  itgsubst  19396  plydivlem1  19673  aannenlem1  19708  taylply2  19747  itgulm  19784  cxpcn  20085  resqrcn  20089  basellem1  20318  mulogsumlem  20680  mulog2sumlem2  20684  selberg2lem  20699  pntrsumo1  20714  zrdivrng  21099  pjssmii  22260  abrexexd  23192  esumcvg  23454  sigaval  23471  orrvcoel  23666  orrvccel  23667  subfaclefac  23707  cvmsss2  23805  cvmopnlem  23809  muldisc  25481  inttaror  25900  prismorcsetlem  25912  prismorcset  25914  cmpmor  25975  iscola2  26092  hmeoclda  26251  ralxpmap  26761  mzpconstmpt  26818  mzpresrename  26828  diophrex  26855  0dioph  26858  anrabdioph  26860  orrabdioph  26861  rabren3dioph  26898  xpexb  27658  fsumcnf  27692  stoweidlem22  27771  aoprssdm  28062  dalemrot  29846  dalem10  29862  arglem1N  30379  cdlemk36  31102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator