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

Theorem syl6eqelr 2372
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 2288 . 2  |-  ( ph  ->  A  =  B )
3 syl6eqelr.2 . 2  |-  B  e.  C
42, 3syl6eqel 2371 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684
This theorem is referenced by:  eusvnfb  4530  wemoiso2  5856  releldm2  6170  mapprc  6776  ixpprc  6837  bren  6871  brdomg  6872  domssex  7022  mapen  7025  ssenen  7035  fodomfib  7136  fi0  7173  dffi3  7184  brwdom  7281  brwdomn0  7283  unxpwdom2  7302  ixpiunwdom  7305  tcmin  7426  tz9.12lem1  7459  rankonid  7501  rankr1id  7534  cardf2  7576  cardid2  7586  carduni  7614  fseqen  7654  acndom  7678  acndom2  7681  alephnbtwn  7698  cardcf  7878  cfeq0  7882  cflim2  7889  coftr  7899  infpssr  7934  hsmexlem5  8056  axdc3lem4  8079  fodomb  8151  ondomon  8185  gruina  8440  ioof  10741  hashbc  11391  hashfacen  11392  fsum  12193  fsumcom2  12237  xpsfrnel2  13467  eqgen  14670  symgbas  14772  dvdsr  15428  asplss  16069  aspsubrg  16071  psrval  16110  clsf  16785  restco  16895  subbascn  16984  is2ndc  17172  ptbasin2  17273  ptbas  17274  indishmph  17489  ufldom  17657  icopnfcld  18277  cnrehmeo  18451  csscld  18676  clsocv  18677  itg2gt0  19115  dvmptadd  19309  dvmptmul  19310  dvmptco  19321  logcn  19994  selberglem1  20694  hmopidmchi  22731  dya2iocbrsiga  23578  inttpemp  25139  prtoptop  25549  fnessref  26293  indexdom  26413  pwslnmlem0  27193  symgfisg  27409  mendval  27491  stirlinglem7  27829  dicfnN  31373
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator