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

Theorem syl6eqelr 2385
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 2301 . 2  |-  ( ph  ->  A  =  B )
3 syl6eqelr.2 . 2  |-  B  e.  C
42, 3syl6eqel 2384 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:  eusvnfb  4546  wemoiso2  5872  releldm2  6186  mapprc  6792  ixpprc  6853  bren  6887  brdomg  6888  domssex  7038  mapen  7041  ssenen  7051  fodomfib  7152  fi0  7189  dffi3  7200  brwdom  7297  brwdomn0  7299  unxpwdom2  7318  ixpiunwdom  7321  tcmin  7442  tz9.12lem1  7475  rankonid  7517  rankr1id  7550  cardf2  7592  cardid2  7602  carduni  7630  fseqen  7670  acndom  7694  acndom2  7697  alephnbtwn  7714  cardcf  7894  cfeq0  7898  cflim2  7905  coftr  7915  infpssr  7950  hsmexlem5  8072  axdc3lem4  8095  fodomb  8167  ondomon  8201  gruina  8456  ioof  10757  hashbc  11407  hashfacen  11408  fsum  12209  fsumcom2  12253  xpsfrnel2  13483  eqgen  14686  symgbas  14788  dvdsr  15444  asplss  16085  aspsubrg  16087  psrval  16126  clsf  16801  restco  16911  subbascn  17000  is2ndc  17188  ptbasin2  17289  ptbas  17290  indishmph  17505  ufldom  17673  icopnfcld  18293  cnrehmeo  18467  csscld  18692  clsocv  18693  itg2gt0  19131  dvmptadd  19325  dvmptmul  19326  dvmptco  19337  logcn  20010  selberglem1  20710  hmopidmchi  22747  dya2iocbrsiga  23593  fprod  24164  inttpemp  25242  prtoptop  25652  fnessref  26396  indexdom  26516  pwslnmlem0  27296  symgfisg  27512  mendval  27594  stirlinglem7  27932  dicfnN  31995
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