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

Theorem syl6eqelr 2919
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 2824 . 2 (𝜑𝐴 = 𝐵)
3 syl6eqelr.2 . 2 𝐵𝐶
42, 3syl6eqel 2918 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890
This theorem is referenced by:  wemoiso2  7664  releldm2  7731  mapprc  8399  ixpprc  8471  bren  8506  brdomg  8507  domssex  8666  mapen  8669  ssenen  8679  fodomfib  8786  fi0  8872  dffi3  8883  brwdom  9019  brwdomn0  9021  unxpwdom2  9040  ixpiunwdom  9043  tcmin  9171  rankonid  9246  rankr1id  9279  cardf2  9360  cardid2  9370  carduni  9398  fseqen  9441  acndom  9465  acndom2  9468  alephnbtwn  9485  cardcf  9662  cfeq0  9666  cflim2  9673  coftr  9683  infpssr  9718  hsmexlem5  9840  axdc3lem4  9863  fodomb  9936  ondomon  9973  gruina  10228  ioof  12823  hashbc  13799  hashfacen  13800  trclun  14362  zsum  15063  fsum  15065  fprod  15283  eqgen  18271  symgbas  18436  symgfisg  18525  dvdsr  19325  asplss  20031  aspsubrg  20033  psrval  20070  clsf  21584  restco  21700  subbascn  21790  is2ndc  21982  ptbasin2  22114  ptbas  22115  indishmph  22334  ufldom  22498  cnextfres1  22604  ussid  22796  icopnfcld  23303  cnrehmeo  23484  csscld  23779  clsocv  23780  itg2gt0  24288  dvmptadd  24484  dvmptmul  24485  dvmptco  24496  logcn  25157  selberglem1  26048  hmopidmchi  29855  sigagensiga  31299  dya2iocbrsiga  31432  dya2icobrsiga  31433  logdivsqrle  31820  fnessref  33602  unirep  34869  indexdom  34890  dicfnN  38199  pwslnmlem0  39569  mendval  39661  icof  41358  dvsubf  42074  dvdivf  42083  itgsinexplem1  42115  stirlinglem7  42242  fourierdlem73  42341  fouriersw  42393  ovolval4lem1  42808
  Copyright terms: Public domain W3C validator