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

Theorem syl6eqelr 2493
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 2409 . 2  |-  ( ph  ->  A  =  B )
3 syl6eqelr.2 . 2  |-  B  e.  C
42, 3syl6eqel 2492 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721
This theorem is referenced by:  eusvnfb  4678  wemoiso2  6038  releldm2  6356  mapprc  6981  ixpprc  7042  bren  7076  brdomg  7077  domssex  7227  mapen  7230  ssenen  7240  fodomfib  7345  fi0  7383  dffi3  7394  brwdom  7491  brwdomn0  7493  unxpwdom2  7512  ixpiunwdom  7515  tcmin  7636  tz9.12lem1  7669  rankonid  7711  rankr1id  7744  cardf2  7786  cardid2  7796  carduni  7824  fseqen  7864  acndom  7888  acndom2  7891  alephnbtwn  7908  cardcf  8088  cfeq0  8092  cflim2  8099  coftr  8109  infpssr  8144  hsmexlem5  8266  axdc3lem4  8289  fodomb  8360  ondomon  8394  gruina  8649  ioof  10958  hashbc  11657  hashfacen  11658  fsum  12469  fsumcom2  12513  xpsfrnel2  13745  eqgen  14948  symgbas  15050  dvdsr  15706  asplss  16343  aspsubrg  16345  psrval  16384  clsf  17067  restco  17182  subbascn  17272  is2ndc  17462  ptbasin2  17563  ptbas  17564  indishmph  17783  ufldom  17947  cnextfres  18052  ussid  18243  icopnfcld  18755  cnrehmeo  18931  csscld  19156  clsocv  19157  itg2gt0  19605  dvmptadd  19799  dvmptmul  19800  dvmptco  19811  logcn  20491  selberglem1  21192  hmopidmchi  23607  ctex  24053  sigagensiga  24477  dya2iocbrsiga  24578  dya2icobrsiga  24579  fprod  25220  fprodcom2  25261  fnessref  26263  indexdom  26326  pwslnmlem0  27061  symgfisg  27277  mendval  27359  itgsinexplem1  27615  stirlinglem7  27696  dicfnN  31666
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400
  Copyright terms: Public domain W3C validator