Theorem eldifsni 4156

Description: Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)

Assertion

Ref	Expression
eldifsni

Proof of Theorem eldifsni

Step	Hyp	Ref	Expression
1		eldifsn 4155	. 2
2	1	simprbi 464	1

Syntax hints:  ->wi 4  e.wcel 1818  =/=wne 2652  \cdif 3472  {csn 4029

This theorem is referenced by:  neldifsn  4157  suppss2OLD  6530  suppssfvOLD  6531  suppssov1OLD  6532  suppssov1  6951  suppss2  6953  suppssfv  6955  sniffsupp  7889  elfi2  7894  fifo  7912  en2other2  8408  finacn  8452  acndom2  8456  dfacacn  8542  kmlem11  8561  acncc  8841  axdc2lem  8849  1div0  10233  expne0i  12198  incexc  13649  oddprm  14339  firest  14830  symgextf1lem  16445  pmtrmvd  16481  efgsp1  16755  efgredlem  16765  gsummpt1n0  16992  dprdfid  17057  dprdfidOLD  17064  dprdres  17075  dprd2da  17091  dmdprdsplit2lem  17094  ablfac1b  17121  lvecinv  17759  lspsncmp  17762  lspsneq  17768  lspsneu  17769  lspdisjb  17772  lspexch  17775  lvecindp  17784  lvecindp2  17785  ringelnzr  17914  fidomndrnglem  17955  psrridm  18058  psrridmOLD  18059  mvridlemOLD  18075  mplsubrg  18102  mplmon  18125  mplmonmul  18126  mplcoe3OLD  18129  mplcoe2OLD  18133  evlslem3  18183  coe1tmmul  18318  uvcff  18822  frlmssuvc2  18826  frlmssuvc2OLD  18828  frlmup2  18833  lindfrn  18856  f1lindf  18857  dmatmul  18999  1marepvsma1  19085  mdetrsca2  19106  mdetrlin2  19109  mdetunilem5  19118  mdetunilem9  19122  maducoeval2  19142  gsummatr01lem3  19159  gsummatr01lem4  19160  gsummatr01  19161  ptpjpre2  20081  ptcmplem2  20553  i1fmullem  22101  itg1addlem4  22106  itg1addlem5  22107  i1fmulc  22110  itg1mulc  22111  i1fres  22112  itg10a  22117  itg1climres  22121  mbfi1fseqlem4  22125  ellimc2  22281  dvcnp2  22323  dvaddbr  22341  dvmulbr  22342  dvcobr  22349  dvcjbr  22352  dvrec  22358  dvcnvlem  22377  dvexp3  22379  dveflem  22380  ftc1lem6  22442  deg1n0ima  22489  ig1peu  22572  plyeq0lem  22607  dgrlem  22626  dgrlb  22633  coemulhi  22651  fta1  22704  aannenlem2  22725  tayl0  22757  taylthlem2  22769  abelthlem7  22833  dcubic  23177  rlimcnp  23295  efrlim  23299  muinv  23469  logexprlim  23500  lgslem1  23571  lgsqr  23621  lgseisenlem2  23625  lgseisenlem4  23627  lgseisen  23628  lgsquadlem1  23629  lgsquad2  23635  m1lgs  23637  dchrisum0re  23698  dchrisum0lema  23699  dchrisum0lem2  23703  dchrisum0lem3  23704  umgran0  24320  umgraex  24323  cusgraexi  24468  frghash2spot  25063  1div0apr  25176  suppss2f  27477  disjdsct  27521  signstfvneq0  28529  subfacp1lem1  28623  circum  29040  dvtan  30065  ftc1cnnc  30089  ftc1anclem3  30092  neibastop1  30177  rrndstprj2  30327  aomclem2  31001  mpaaeu  31099  sdrgacs  31150  cntzsdrg  31151  deg1mhm  31167  radcnvrat  31195  bccm1k  31247  icoiccdif  31564  fprodn0f  31594  climrec  31609  climdivf  31618  lptre2pt  31646  0ellimcdiv  31655  limclner  31657  reclimc  31659  divcncf  31686  cncficcgt0  31691  dvrecg  31707  fperdvper  31715  dvdivcncf  31724  dvnmul  31740  stoweidlem57  31839  dirkercncflem1  31885  fourierdlem24  31913  fourierdlem62  31951  fourierdlem66  31955  elaa2  32017  etransclem35  32052  etransclem47  32064  lindssnlvec  33087  elogb  33169  bj-xpnzexb  34518  lshpne0  34711  lsatcv0  34756  lsat0cv  34758  lkreqN  34895  lkrlspeqN  34896  dochnel  37120  djhcvat42  37142  dochsnkr  37199  dochsnkr2cl  37201  lcfl6lem  37225  lcfl8b  37231  lcfrlem16  37285  lcfrlem25  37294  lcfrlem27  37296  lcfrlem33  37302  lcfrlem37  37306  mapdn0  37396  mapdpglem24  37431  mapdindp1  37447  mapdhval2  37453  hdmap1val2  37528  hdmapnzcl  37575  hdmap14lem1  37598  hdmap14lem4a  37601  hdmap14lem6  37603  hgmaprnlem1N  37626  hdmapip1  37646  hgmapvvlem1  37653  hgmapvvlem2  37654

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-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-sn 4030