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

Theorem syl5eqelr 2381
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 2300 . 2  |-  A  =  B
3 syl5eqelr.2 . 2  |-  ( ph  ->  B  e.  C )
42, 3syl5eqel 2380 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696
This theorem is referenced by:  dmrnssfld  4954  cnvexg  5224  resfunexgALT  5754  abrexexg  5780  abrexex2g  5784  oprssdm  6018  offval  6101  imafi  7164  abrexfi  7172  ssfii  7188  wdomima2g  7316  unxpwdom2  7318  tskwe  7599  ac10ct  7677  fin23lem28  7982  fin23lem30  7984  axcclem  8099  distrlem4pr  8666  iccshftr  10785  iccshftl  10787  iccdil  10789  icccntr  10791  wrdexb  11465  o1res  12050  exprmfct  12805  infpnlem1  12973  4sqlem13  13020  0ram  13083  ismred2  13521  mreexexlem2d  13563  mreexexlem4d  13565  acsfn1c  13580  acsfn2  13581  ssclem  13712  submacs  14458  efgrcl  15040  dprd2da  15293  irredlmul  15506  lidlrsppropd  15998  issubassa  16080  ply1crng  16293  ply1rng  16342  ply1lmod  16346  chrcl  16496  css1  16606  0opn  16666  fctop2  16758  difopn  16787  tgrest  16906  ordtbas2  16937  ordtopn3  16942  ordtcld3  16945  t1ficld  17071  resthauslem  17107  kgentopon  17249  txbasex  17277  txcnpi  17318  txdis1cn  17345  pthaus  17348  txkgen  17362  cnmptid  17371  cnmptc  17372  cnmpt1st  17378  cnmpt2nd  17379  cnmpt2c  17380  cnmptkc  17389  txcon  17399  hmeoima  17472  hmeocld  17474  xkohmeo  17522  filufint  17631  fin1aufil  17643  flftg  17707  ptcmplem2  17763  tmdmulg  17791  tmdgsum2  17795  symgtgp  17800  submtmd  17803  ghmcnp  17813  divstgpopn  17818  divstgplem  17819  nrginvrcn  18218  fsumcn  18390  fsum2cn  18391  expcn  18392  cnheibor  18469  evth2  18474  csscld  18692  clsocv  18693  ovoliun2  18881  volfiniun  18920  dyadmbl  18971  mbfeqalem  19013  mbfss  19017  ismbf3d  19025  mbfadd  19032  i1f0rn  19053  mbfmul  19097  itg2seq  19113  itg2monolem2  19122  itg2monolem3  19123  itg2mono  19124  itgreval  19167  itgge0  19181  itgss3  19185  iblconst  19188  itgconst  19189  ibladdlem  19190  itgfsum  19197  iblabslem  19198  itgabs  19205  mvth  19355  lhop1lem  19376  dvfsumle  19384  dvfsumlem2  19390  ftc1lem4  19402  itgparts  19410  itgsubstlem  19411  itgsubst  19412  plydivlem1  19689  aannenlem1  19724  taylply2  19763  itgulm  19800  cxpcn  20101  resqrcn  20105  basellem1  20334  mulogsumlem  20696  mulog2sumlem2  20700  selberg2lem  20715  pntrsumo1  20730  zrdivrng  21115  pjssmii  22276  abrexexd  23207  esumcvg  23469  sigaval  23486  orrvcoel  23681  orrvccel  23682  subfaclefac  23722  cvmsss2  23820  cvmopnlem  23824  ibladdnclem  25007  iblabsnclem  25014  itgabsnc  25020  ftc1cnnclem  25024  muldisc  25584  inttaror  26003  prismorcsetlem  26015  prismorcset  26017  cmpmor  26078  iscola2  26195  hmeoclda  26354  ralxpmap  26864  mzpconstmpt  26921  mzpresrename  26931  diophrex  26958  0dioph  26961  anrabdioph  26963  orrabdioph  26964  rabren3dioph  27001  xpexb  27761  fsumcnf  27795  stoweidlem22  27874  aoprssdm  28170  opabex3d  28190  opabbrex  28191  dalemrot  30468  dalem10  30484  arglem1N  31001  cdlemk36  31724
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator