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

Theorem syl6eqelr 2739
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl6eqelr.1 (𝜑𝐵 = 𝐴)
syl6eqelr.2 𝐵𝐶
Assertion
Ref Expression
syl6eqelr (𝜑𝐴𝐶)

Proof of Theorem syl6eqelr
StepHypRef Expression
1 syl6eqelr.1 . . 3 (𝜑𝐵 = 𝐴)
21eqcomd 2657 . 2 (𝜑𝐴 = 𝐵)
3 syl6eqelr.2 . 2 𝐵𝐶
42, 3syl6eqel 2738 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647
This theorem is referenced by:  wemoiso2  7196  releldm2  7262  mapprc  7903  ixpprc  7971  bren  8006  brdomg  8007  ctex  8012  domssex  8162  mapen  8165  ssenen  8175  fodomfib  8281  fi0  8367  dffi3  8378  brwdom  8513  brwdomn0  8515  unxpwdom2  8534  ixpiunwdom  8537  tcmin  8655  rankonid  8730  rankr1id  8763  cardf2  8807  cardid2  8817  carduni  8845  fseqen  8888  acndom  8912  acndom2  8915  alephnbtwn  8932  cardcf  9112  cfeq0  9116  cflim2  9123  coftr  9133  infpssr  9168  hsmexlem5  9290  axdc3lem4  9313  fodomb  9386  ondomon  9423  gruina  9678  ioof  12309  hashbc  13275  hashfacen  13276  trclun  13799  zsum  14493  fsum  14495  fsumcom2OLD  14550  fprod  14715  fprodcom2OLD  14759  xpsfrnel2  16272  eqgen  17694  symgbas  17846  symgfisg  17934  dvdsr  18692  asplss  19377  aspsubrg  19379  psrval  19410  clsf  20900  restco  21016  subbascn  21106  is2ndc  21297  ptbasin2  21429  ptbas  21430  indishmph  21649  ufldom  21813  cnextfres1  21919  ussid  22111  icopnfcld  22618  cnrehmeo  22799  csscld  23094  clsocv  23095  itg2gt0  23572  dvmptadd  23768  dvmptmul  23769  dvmptco  23780  logcn  24438  selberglem1  25279  hmopidmchi  29138  sigagensiga  30332  dya2iocbrsiga  30465  dya2icobrsiga  30466  logdivsqrle  30856  fnessref  32477  unirep  33637  indexdom  33659  dicfnN  36789  pwslnmlem0  37978  mendval  38070  icof  39725  dvsubf  40446  dvdivf  40455  itgsinexplem1  40487  stirlinglem7  40615  fourierdlem73  40714  fouriersw  40766  ovolval4lem1  41184
  Copyright terms: Public domain W3C validator