Theorem syl6eqelr 2511

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

Step	Hyp	Ref	Expression
1		syl6eqelr.1	. . 3
2	1	eqcomd 2427	. 2
3		syl6eqelr.2	. 2
4	2, 3	syl6eqel 2510	1

Syntax hints:  ->wi 4  =wceq 1687  e.wcel 1749

This theorem is referenced by:  wemoiso2  6532  releldm2  6593  mapprc  7179  ixpprc  7243  bren  7278  brdomg  7279  domssex  7431  mapen  7434  ssenen  7444  fodomfib  7550  fi0  7617  dffi3  7628  brwdom  7729  brwdomn0  7731  unxpwdom2  7750  ixpiunwdom  7753  tcmin  7908  rankonid  7983  rankr1id  8016  cardf2  8060  cardid2  8070  carduni  8098  fseqen  8144  acndom  8168  acndom2  8171  alephnbtwn  8188  cardcf  8368  cfeq0  8372  cflim2  8379  coftr  8389  infpssr  8424  hsmexlem5  8546  axdc3lem4  8569  fodomb  8640  ondomon  8674  gruina  8931  ioof  11332  hashbc  12147  hashfacen  12148  zsum  13136  fsum  13138  fsumcom2  13182  xpsfrnel2  14443  eqgen  15671  symgbas  15822  symgfisg  15911  dvdsr  16561  asplss  17208  aspsubrg  17210  psrval  17249  clsf  18356  restco  18472  subbascn  18562  is2ndc  18754  ptbasin2  18855  ptbas  18856  indishmph  19075  ufldom  19239  cnextfres  19344  ussid  19535  icopnfcld  20047  cnrehmeo  20225  csscld  20461  clsocv  20462  itg2gt0  20938  dvmptadd  21134  dvmptmul  21135  dvmptco  21146  logcn  21833  selberglem1  22535  hmopidmchi  25234  ctex  25688  sigagensiga  26293  dya2iocbrsiga  26399  dya2icobrsiga  26400  fprod  27156  fprodcom2  27197  fnessref  28236  unirep  28277  indexdom  28299  pwslnmlem0  29117  mendval  29213  itgsinexplem1  29468  stirlinglem7  29549  wlkelwrd  29954  wlkcompim  29961  clwlkcompim  30101  dicfnN  34265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-12 1785  ax-ext 2403

This theorem depends on definitions:  df-bi 179  df-an 364  df-ex 1582  df-cleq 2415  df-clel 2418