Theorem eldifsni 4478

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 4474	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
2	1	simprbi 490	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴 ≠ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2155   ≠ wne 2937   ∖ cdif 3731  {csn 4336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-v 3352  df-dif 3737  df-sn 4337

This theorem is referenced by:  neldifsn  4479  suppssov1  7532  suppss2  7534  suppssfv  7536  sniffsupp  8524  elfi2  8529  fifo  8547  en2other2  9085  finacn  9126  acndom2  9130  dfacacn  9218  kmlem11  9237  acncc  9517  axdc2lem  9525  1div0  10942  expne0i  13102  incexc  14856  fprodn0f  15007  oddprm  15797  firest  16362  symgextf1lem  18106  pmtrmvd  18142  efgsp1  18417  efgredlem  18428  efgredlemOLD  18429  gsummpt1n0  18633  dprdfid  18686  dprdres  18697  dprd2da  18711  dmdprdsplit2lem  18714  ablfac1b  18739  lvecinv  19388  lspsncmp  19391  lspsneq  19397  lspsneu  19398  lspdisjb  19401  lspexch  19405  lvecindp2  19415  ringelnzr  19543  fidomndrnglem  19583  psrridm  19681  mplsubrg  19717  mplmon  19740  mplmonmul  19741  evlslem3  19790  coe1tmmul  19923  uvcff  20409  frlmssuvc2  20413  frlmup2  20417  lindfrn  20439  f1lindf  20440  dmatmul  20583  1marepvsma1  20669  mdetrsca2  20690  mdetrlin2  20693  mdetunilem5  20702  mdetunilem9  20706  maducoeval2  20726  gsummatr01lem3  20744  gsummatr01lem4  20745  gsummatr01  20746  ptpjpre2  21666  ptcmplem2  22139  divcncf  23508  i1fmullem  23755  itg1addlem4  23760  itg1addlem5  23761  i1fmulc  23764  itg1mulc  23765  i1fres  23766  itg10a  23771  itg1climres  23775  mbfi1fseqlem4  23779  ellimc2  23935  dvcnp2  23977  dvaddbr  23995  dvmulbr  23996  dvcobr  24003  dvcjbr  24006  dvrec  24012  dvrecg  24030  dvcnvlem  24033  dvexp3  24035  dveflem  24036  ftc1lem6  24098  deg1n0ima  24143  ig1peu  24225  plyeq0lem  24260  dgrlem  24279  dgrlb  24286  coemulhi  24304  fta1  24357  aannenlem2  24378  tayl0  24410  taylthlem2  24422  abelthlem7  24486  dcubic  24867  rlimcnp  24986  efrlim  24990  muinv  25213  logexprlim  25244  lgslem1  25316  lgsqr  25370  lgseisenlem2  25395  lgseisenlem4  25397  lgseisen  25398  lgsquadlem1  25399  lgsquad2  25405  m1lgs  25407  dchrisum0re  25496  dchrisum0lema  25497  dchrisum0lem2  25501  dchrisum0lem3  25502  uhgrn0  26242  upgrn0  26264  upgrex  26267  numedglnl  26320  upgrreslem  26478  isuvtx  26581  isuvtxaOLD  26582  cusgrexilem2  26632  cusgrexi  26633  structtocusgr  26636  cusgrfilem2  26646  frgrhash2wsp  27615  1div0apr  27786  disjdsct  29932  signstfvneq0  31102  subfacp1lem1  31612  circum  32017  neibastop1  32800  bj-xpnzexb  33378  bj-restn0b  33475  curf  33814  poimirlem2  33838  poimirlem24  33860  poimirlem25  33861  dvtan  33886  ftc1cnnc  33910  ftc1anclem3  33913  rrndstprj2  34055  lsat0cv  34992  lkreqN  35129  lkrlspeqN  35130  dochnel  37352  djhcvat42  37374  dochsnkr  37431  dochsnkr2cl  37433  lcfl6lem  37457  lcfl8b  37463  lcfrlem16  37517  lcfrlem25  37526  lcfrlem27  37528  lcfrlem33  37534  lcfrlem37  37538  mapdn0  37628  mapdpglem24  37663  mapdindp1  37679  mapdhval2  37685  hdmap1val2  37759  hdmapnzcl  37804  hdmap14lem1  37827  hdmap14lem4a  37830  hdmap14lem6  37832  hgmaprnlem1N  37855  hdmapip1  37875  hgmapvvlem1  37882  hgmapvvlem2  37883  aomclem2  38305  mpaaeu  38400  sdrgacs  38451  cntzsdrg  38452  deg1mhm  38465  clsk3nimkb  39015  gneispace  39109  radcnvrat  39190  bccm1k  39218  disjf1o  40028  supminfxr2  40339  icoiccdif  40392  climrec  40476  climdivf  40485  lptre2pt  40513  0ellimcdiv  40522  limclner  40524  reclimc  40526  cnrefiisplem  40696  cncficcgt0  40742  fperdvper  40774  dvdivcncf  40783  dvnmul  40799  stoweidlem57  40914  dirkercncflem1  40960  fourierdlem24  40988  fourierdlem62  41025  fourierdlem66  41029  elaa2  41091  etransclem35  41126  etransclem47  41138  meadjiunlem  41322  ovnhoilem1  41458  hspmbllem1  41483  fmtnoprmfac1lem  42155  lindssnlvec  42947  logcxp0  43001