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

Theorem syl6eqelr 2479
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl6eqelr.1  |-  ( ph  ->  B  =  A )
syl6eqelr.2  |-  B  e.  C
Assertion
Ref Expression
syl6eqelr  |-  ( ph  ->  A  e.  C )

Proof of Theorem syl6eqelr
StepHypRef Expression
1 syl6eqelr.1 . . 3  |-  ( ph  ->  B  =  A )
21eqcomd 2390 . 2  |-  ( ph  ->  A  =  B )
3 syl6eqelr.2 . 2  |-  B  e.  C
42, 3syl6eqel 2478 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399    e. wcel 1826
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621  df-cleq 2374  df-clel 2377
This theorem is referenced by:  wemoiso2  6685  releldm2  6749  mapprc  7342  ixpprc  7409  bren  7444  brdomg  7445  domssex  7597  mapen  7600  ssenen  7610  fodomfib  7715  fi0  7795  dffi3  7806  brwdom  7908  brwdomn0  7910  unxpwdom2  7929  ixpiunwdom  7932  tcmin  8085  rankonid  8160  rankr1id  8193  cardf2  8237  cardid2  8247  carduni  8275  fseqen  8321  acndom  8345  acndom2  8348  alephnbtwn  8365  cardcf  8545  cfeq0  8549  cflim2  8556  coftr  8566  infpssr  8601  hsmexlem5  8723  axdc3lem4  8746  fodomb  8817  ondomon  8851  gruina  9107  ioof  11543  hashbc  12406  hashfacen  12407  trclun  12852  zsum  13542  fsum  13544  fsumcom2  13591  fprod  13750  fprodcom2  13790  xpsfrnel2  14972  eqgen  16371  symgbas  16522  symgfisg  16610  dvdsr  17408  asplss  18091  aspsubrg  18093  psrval  18124  clsf  19634  restco  19751  subbascn  19841  is2ndc  20032  ptbasin2  20164  ptbas  20165  indishmph  20384  ufldom  20548  cnextfres  20653  ussid  20848  icopnfcld  21360  cnrehmeo  21538  csscld  21774  clsocv  21775  itg2gt0  22252  dvmptadd  22448  dvmptmul  22449  dvmptco  22460  logcn  23115  selberglem1  23847  wlkcompim  24647  wlkelwrd  24651  clwlkcompim  24885  hmopidmchi  27186  ctex  27680  sigagensiga  28290  dya2iocbrsiga  28402  dya2icobrsiga  28403  fnessref  30341  unirep  30369  indexdom  30391  pwslnmlem0  31203  mendval  31300  dvsubf  31875  fperdvper  31881  dvdivf  31885  itgsinexplem1  31918  stirlinglem7  32028  fourierdlem73  32128  fouriersw  32180  dicfnN  37323
  Copyright terms: Public domain W3C validator