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

Theorem syl5eqelr 2523
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 2442 . 2  |-  A  =  B
3 syl5eqelr.2 . 2  |-  ( ph  ->  B  e.  C )
42, 3syl5eqel 2522 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726
This theorem is referenced by:  dmrnssfld  5131  cnvexg  5407  resfunexgALT  5960  abrexexg  5986  abrexex2g  5990  opabex3d  5991  opabbrex  6120  oprssdm  6230  offval  6314  imafi  7401  abrexfi  7409  ssfii  7426  wdomima2g  7556  unxpwdom2  7558  tskwe  7839  ac10ct  7917  fin23lem28  8222  fin23lem30  8224  axcclem  8339  distrlem4pr  8905  iccshftr  11032  iccshftl  11034  iccdil  11036  icccntr  11038  wrdexb  11765  o1res  12356  exprmfct  13112  infpnlem1  13280  4sqlem13  13327  0ram  13390  ismred2  13830  mreexexlem2d  13872  mreexexlem4d  13874  acsfn1c  13889  acsfn2  13890  ssclem  14021  submacs  14767  efgrcl  15349  dprd2da  15602  irredlmul  15815  lidlrsppropd  16303  issubassa  16385  ply1crng  16598  ply1rng  16644  ply1lmod  16648  chrcl  16809  css1  16919  0opn  16979  fctop2  17071  difopn  17100  tgrest  17225  ordtbas2  17257  ordtopn3  17262  ordtcld3  17265  t1ficld  17393  resthauslem  17429  kgentopon  17572  txbasex  17600  txcnpi  17642  txdis1cn  17669  pthaus  17672  txkgen  17686  cnmptid  17695  cnmptc  17696  cnmpt1st  17702  cnmpt2nd  17703  cnmpt2c  17704  cnmptkc  17713  txcon  17723  hmeoima  17799  hmeocld  17801  xkohmeo  17849  filufint  17954  fin1aufil  17966  flftg  18030  ptcmplem2  18086  tmdmulg  18124  tmdgsum2  18128  symgtgp  18133  submtmd  18136  ghmcnp  18146  divstgpopn  18151  divstgplem  18152  ust0  18251  nrginvrcn  18729  fsumcn  18902  fsum2cn  18903  expcn  18904  cnheibor  18982  evth2  18987  csscld  19205  clsocv  19206  ovoliun2  19404  volfiniun  19443  dyadmbl  19494  mbfeqalem  19536  mbfss  19540  ismbf3d  19548  mbfadd  19555  i1f0rn  19576  mbfmul  19620  itg2seq  19636  itg2monolem2  19645  itg2monolem3  19646  itg2mono  19647  itgreval  19690  itgge0  19704  itgss3  19708  iblconst  19711  itgconst  19712  ibladdlem  19713  itgfsum  19720  iblabslem  19721  itgabs  19728  mvth  19878  lhop1lem  19899  dvfsumle  19907  dvfsumlem2  19913  ftc1lem4  19925  itgparts  19933  itgsubstlem  19934  itgsubst  19935  plydivlem1  20212  aannenlem1  20247  taylply2  20286  itgulm  20326  cxpcn  20631  resqrcn  20635  basellem1  20865  mulogsumlem  21227  mulog2sumlem2  21231  selberg2lem  21246  pntrsumo1  21261  nbgracnvfv  21452  zrdivrng  22022  pjssmii  23185  abrexexd  23992  esumcvg  24478  sigaval  24495  sigaclfu2  24506  measinb2  24579  braew  24595  sibfof  24656  sitgclg  24658  orrvcoel  24725  orrvccel  24726  subfaclefac  24864  cvmsss2  24963  cvmopnlem  24967  mblfinlem1  26245  cnambfre  26257  ibladdnclem  26263  iblabsnclem  26270  itgabsnc  26276  ftc1cnnclem  26280  ftc1anclem4  26285  ftc1anclem5  26286  ftc1anclem6  26287  ftc1anclem7  26288  ftc2nc  26291  areacirc  26299  hmeoclda  26338  ralxpmap  26744  mzpconstmpt  26799  mzpresrename  26809  diophrex  26836  0dioph  26839  anrabdioph  26841  orrabdioph  26842  rabren3dioph  26878  xpexb  27636  fsumcnf  27670  aoprssdm  28044  dalemrot  30516  dalem10  30532  arglem1N  31049  cdlemk36  31772
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2431  df-clel 2434
  Copyright terms: Public domain W3C validator