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

Theorem syl6eqelr 2538
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 2449 . 2  |-  ( ph  ->  A  =  B )
3 syl6eqelr.2 . 2  |-  B  e.  C
42, 3syl6eqel 2537 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1381    e. wcel 1802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-cleq 2433  df-clel 2436
This theorem is referenced by:  wemoiso2  6767  releldm2  6831  mapprc  7422  ixpprc  7488  bren  7523  brdomg  7524  domssex  7676  mapen  7679  ssenen  7689  fodomfib  7798  fi0  7878  dffi3  7889  brwdom  7991  brwdomn0  7993  unxpwdom2  8012  ixpiunwdom  8015  tcmin  8170  rankonid  8245  rankr1id  8278  cardf2  8322  cardid2  8332  carduni  8360  fseqen  8406  acndom  8430  acndom2  8433  alephnbtwn  8450  cardcf  8630  cfeq0  8634  cflim2  8641  coftr  8651  infpssr  8686  hsmexlem5  8808  axdc3lem4  8831  fodomb  8902  ondomon  8936  gruina  9194  ioof  11626  hashbc  12476  hashfacen  12477  zsum  13514  fsum  13516  fsumcom2  13563  xpsfrnel2  14834  eqgen  16123  symgbas  16274  symgfisg  16362  dvdsr  17163  asplss  17846  aspsubrg  17848  psrval  17879  clsf  19415  restco  19531  subbascn  19621  is2ndc  19813  ptbasin2  19945  ptbas  19946  indishmph  20165  ufldom  20329  cnextfres  20434  ussid  20629  icopnfcld  21141  cnrehmeo  21319  csscld  21555  clsocv  21556  itg2gt0  22033  dvmptadd  22229  dvmptmul  22230  dvmptco  22241  logcn  22893  selberglem1  23595  wlkcompim  24391  wlkelwrd  24395  clwlkcompim  24629  hmopidmchi  26935  ctex  27396  sigagensiga  28007  dya2iocbrsiga  28112  dya2icobrsiga  28113  fprod  29041  fprodcom2  29082  fnessref  30143  unirep  30171  indexdom  30193  pwslnmlem0  31005  mendval  31101  dvsubf  31609  fperdvper  31615  dvdivf  31619  itgsinexplem1  31638  stirlinglem7  31747  fourierdlem73  31847  fouriersw  31899  dicfnN  36612
  Copyright terms: Public domain W3C validator