Theorem eldifsni 4320

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

Assertion

Ref	Expression
eldifsni	|- ( A e. ( B \ { C } ) -> A =/= C )

Proof of Theorem eldifsni

Step	Hyp	Ref	Expression
1		eldifsn 4317	. 2 |- ( A e. ( B \ { C } ) <-> ( A e. B /\ A =/= C ) )
2	1	simprbi 480	1 |- ( A e. ( B \ { C } ) -> A =/= C )

Syntax hints:   -> wi 4   e. wcel 1990   =/= wne 2794   \ cdif 3571   {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-v 3202  df-dif 3577  df-sn 4178

This theorem is referenced by:  neldifsn  4321  suppssov1  7327  suppss2  7329  suppssfv  7331  sniffsupp  8315  elfi2  8320  fifo  8338  en2other2  8832  finacn  8873  acndom2  8877  dfacacn  8963  kmlem11  8982  acncc  9262  axdc2lem  9270  1div0  10686  expne0i  12892  incexc  14569  fprodn0f  14722  oddprm  15515  firest  16093  symgextf1lem  17840  pmtrmvd  17876  efgsp1  18150  efgredlem  18160  gsummpt1n0  18364  dprdfid  18416  dprdres  18427  dprd2da  18441  dmdprdsplit2lem  18444  ablfac1b  18469  lvecinv  19113  lspsncmp  19116  lspsneq  19122  lspsneu  19123  lspdisjb  19126  lspexch  19129  lvecindp  19138  lvecindp2  19139  ringelnzr  19266  fidomndrnglem  19306  psrridm  19404  mplsubrg  19440  mplmon  19463  mplmonmul  19464  evlslem3  19514  coe1tmmul  19647  uvcff  20130  frlmssuvc2  20134  frlmup2  20138  lindfrn  20160  f1lindf  20161  dmatmul  20303  1marepvsma1  20389  mdetrsca2  20410  mdetrlin2  20413  mdetunilem5  20422  mdetunilem9  20426  maducoeval2  20446  gsummatr01lem3  20463  gsummatr01lem4  20464  gsummatr01  20465  ptpjpre2  21383  ptcmplem2  21857  divcncf  23216  i1fmullem  23461  itg1addlem4  23466  itg1addlem5  23467  i1fmulc  23470  itg1mulc  23471  i1fres  23472  itg10a  23477  itg1climres  23481  mbfi1fseqlem4  23485  ellimc2  23641  dvcnp2  23683  dvaddbr  23701  dvmulbr  23702  dvcobr  23709  dvcjbr  23712  dvrec  23718  dvrecg  23736  dvcnvlem  23739  dvexp3  23741  dveflem  23742  ftc1lem6  23804  deg1n0ima  23849  ig1peu  23931  plyeq0lem  23966  dgrlem  23985  dgrlb  23992  coemulhi  24010  fta1  24063  aannenlem2  24084  tayl0  24116  taylthlem2  24128  abelthlem7  24192  dcubic  24573  rlimcnp  24692  efrlim  24696  muinv  24919  logexprlim  24950  lgslem1  25022  lgsqr  25076  lgseisenlem2  25101  lgseisenlem4  25103  lgseisen  25104  lgsquadlem1  25105  lgsquad2  25111  m1lgs  25113  dchrisum0re  25202  dchrisum0lema  25203  dchrisum0lem2  25207  dchrisum0lem3  25208  uhgrn0  25962  upgrn0  25984  upgrex  25987  numedglnl  26039  upgrreslem  26196  isuvtxa  26295  cusgrexilem2  26338  cusgrexi  26339  structtocusgr  26342  cusgrfilem2  26352  frgrhash2wsp  27196  1div0apr  27324  disjdsct  29480  signstfvneq0  30649  subfacp1lem1  31161  circum  31568  neibastop1  32354  bj-xpnzexb  32948  bj-restn0b  33044  curf  33387  poimirlem2  33411  poimirlem24  33433  poimirlem25  33434  dvtan  33460  ftc1cnnc  33484  ftc1anclem3  33487  rrndstprj2  33630  lshpne0  34273  lsatcv0  34318  lsat0cv  34320  lkreqN  34457  lkrlspeqN  34458  dochnel  36682  djhcvat42  36704  dochsnkr  36761  dochsnkr2cl  36763  lcfl6lem  36787  lcfl8b  36793  lcfrlem16  36847  lcfrlem25  36856  lcfrlem27  36858  lcfrlem33  36864  lcfrlem37  36868  mapdn0  36958  mapdpglem24  36993  mapdindp1  37009  mapdhval2  37015  hdmap1val2  37090  hdmapnzcl  37137  hdmap14lem1  37160  hdmap14lem4a  37163  hdmap14lem6  37165  hgmaprnlem1N  37188  hdmapip1  37208  hgmapvvlem1  37215  hgmapvvlem2  37216  aomclem2  37625  mpaaeu  37720  sdrgacs  37771  cntzsdrg  37772  deg1mhm  37785  clsk3nimkb  38338  gneispace  38432  radcnvrat  38513  bccm1k  38541  disjf1o  39378  supminfxr2  39699  icoiccdif  39750  climrec  39835  climdivf  39844  lptre2pt  39872  0ellimcdiv  39881  limclner  39883  reclimc  39885  cnrefiisplem  40055  cncficcgt0  40101  fperdvper  40133  dvdivcncf  40142  dvnmul  40158  stoweidlem57  40274  dirkercncflem1  40320  fourierdlem24  40348  fourierdlem62  40385  fourierdlem66  40389  elaa2  40451  etransclem35  40486  etransclem47  40498  meadjiunlem  40682  ovnhoilem1  40815  hspmbllem1  40840  fmtnoprmfac1lem  41476  lindssnlvec  42275  logcxp0  42329