Theorem syl6eqelr 2554

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 2465	. 2
3		syl6eqelr.2	. 2
4	2, 3	syl6eqel 2553	1

Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818

This theorem is referenced by:  wemoiso2  6786  releldm2  6850  mapprc  7443  ixpprc  7510  bren  7545  brdomg  7546  domssex  7698  mapen  7701  ssenen  7711  fodomfib  7820  fi0  7900  dffi3  7911  brwdom  8014  brwdomn0  8016  unxpwdom2  8035  ixpiunwdom  8038  tcmin  8193  rankonid  8268  rankr1id  8301  cardf2  8345  cardid2  8355  carduni  8383  fseqen  8429  acndom  8453  acndom2  8456  alephnbtwn  8473  cardcf  8653  cfeq0  8657  cflim2  8664  coftr  8674  infpssr  8709  hsmexlem5  8831  axdc3lem4  8854  fodomb  8925  ondomon  8959  gruina  9217  ioof  11651  hashbc  12502  hashfacen  12503  zsum  13540  fsum  13542  fsumcom2  13589  fprod  13748  fprodcom2  13788  xpsfrnel2  14962  eqgen  16254  symgbas  16405  symgfisg  16493  dvdsr  17295  asplss  17978  aspsubrg  17980  psrval  18011  clsf  19549  restco  19665  subbascn  19755  is2ndc  19947  ptbasin2  20079  ptbas  20080  indishmph  20299  ufldom  20463  cnextfres  20568  ussid  20763  icopnfcld  21275  cnrehmeo  21453  csscld  21689  clsocv  21690  itg2gt0  22167  dvmptadd  22363  dvmptmul  22364  dvmptco  22375  logcn  23028  selberglem1  23730  wlkcompim  24526  wlkelwrd  24530  clwlkcompim  24764  hmopidmchi  27070  ctex  27531  sigagensiga  28141  dya2iocbrsiga  28246  dya2icobrsiga  28247  fnessref  30175  unirep  30203  indexdom  30225  pwslnmlem0  31037  mendval  31132  dvsubf  31709  fperdvper  31715  dvdivf  31719  itgsinexplem1  31752  stirlinglem7  31862  fourierdlem73  31962  fouriersw  32014  dicfnN  36910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452