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

Theorem syl6eqelr 2526
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 2437 . 2  |-  ( ph  ->  A  =  B )
3 syl6eqelr.2 . 2  |-  B  e.  C
42, 3syl6eqel 2525 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-cleq 2421  df-clel 2424
This theorem is referenced by:  wemoiso2  6793  releldm2  6857  mapprc  7484  ixpprc  7551  bren  7586  brdomg  7587  domssex  7739  mapen  7742  ssenen  7752  fodomfib  7857  fi0  7940  dffi3  7951  brwdom  8082  brwdomn0  8084  unxpwdom2  8103  ixpiunwdom  8106  tcmin  8224  rankonid  8299  rankr1id  8332  cardf2  8376  cardid2  8386  carduni  8414  fseqen  8456  acndom  8480  acndom2  8483  alephnbtwn  8500  cardcf  8680  cfeq0  8684  cflim2  8691  coftr  8701  infpssr  8736  hsmexlem5  8858  axdc3lem4  8881  fodomb  8952  ondomon  8986  gruina  9242  ioof  11732  hashbc  12611  hashfacen  12612  trclun  13057  zsum  13762  fsum  13764  fsumcom2  13813  fprod  13973  fprodcom2  14016  xpsfrnel2  15422  eqgen  16821  symgbas  16972  symgfisg  17060  dvdsr  17809  asplss  18488  aspsubrg  18490  psrval  18521  clsf  19994  restco  20111  subbascn  20201  is2ndc  20392  ptbasin2  20524  ptbas  20525  indishmph  20744  ufldom  20908  cnextfres1  21014  ussid  21206  icopnfcld  21699  cnrehmeo  21877  csscld  22113  clsocv  22114  itg2gt0  22595  dvmptadd  22791  dvmptmul  22792  dvmptco  22803  logcn  23457  selberglem1  24246  wlkcompim  25099  wlkelwrd  25103  clwlkcompim  25337  hmopidmchi  27639  ctex  28135  sigagensiga  28802  dya2iocbrsiga  28936  dya2icobrsiga  28937  fnessref  30798  unirep  31743  indexdom  31765  dicfnN  34460  pwslnmlem0  35655  mendval  35748  dvsubf  37356  fperdvper  37362  dvdivf  37366  itgsinexplem1  37399  stirlinglem7  37511  fourierdlem73  37611  fouriersw  37663
  Copyright terms: Public domain W3C validator