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

Theorem syl6eqelr 2530
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 2446 . 2  |-  ( ph  ->  A  =  B )
3 syl6eqelr.2 . 2  |-  B  e.  C
42, 3syl6eqel 2529 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364    e. wcel 1761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-cleq 2434  df-clel 2437
This theorem is referenced by:  wemoiso2  6562  releldm2  6623  mapprc  7214  ixpprc  7280  bren  7315  brdomg  7316  domssex  7468  mapen  7471  ssenen  7481  fodomfib  7587  fi0  7666  dffi3  7677  brwdom  7778  brwdomn0  7780  unxpwdom2  7799  ixpiunwdom  7802  tcmin  7957  rankonid  8032  rankr1id  8065  cardf2  8109  cardid2  8119  carduni  8147  fseqen  8193  acndom  8217  acndom2  8220  alephnbtwn  8237  cardcf  8417  cfeq0  8421  cflim2  8428  coftr  8438  infpssr  8473  hsmexlem5  8595  axdc3lem4  8618  fodomb  8689  ondomon  8723  gruina  8981  ioof  11383  hashbc  12202  hashfacen  12203  zsum  13191  fsum  13193  fsumcom2  13237  xpsfrnel2  14499  eqgen  15727  symgbas  15878  symgfisg  15967  dvdsr  16728  asplss  17378  aspsubrg  17380  psrval  17407  clsf  18611  restco  18727  subbascn  18817  is2ndc  19009  ptbasin2  19110  ptbas  19111  indishmph  19330  ufldom  19494  cnextfres  19599  ussid  19794  icopnfcld  20306  cnrehmeo  20484  csscld  20720  clsocv  20721  itg2gt0  21197  dvmptadd  21393  dvmptmul  21394  dvmptco  21405  logcn  22051  selberglem1  22753  hmopidmchi  25490  ctex  25943  sigagensiga  26520  dya2iocbrsiga  26626  dya2icobrsiga  26627  fprod  27383  fprodcom2  27424  fnessref  28490  unirep  28531  indexdom  28553  pwslnmlem0  29369  mendval  29465  itgsinexplem1  29719  stirlinglem7  29800  wlkelwrd  30205  wlkcompim  30212  clwlkcompim  30352  dicfnN  34550
  Copyright terms: Public domain W3C validator