Theorem eldifsni 4748

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933   ∖ cdif 3900  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3444  df-dif 3906  df-sn 4583

This theorem is referenced by:  eldifsnneq  4749  neldifsn  4750  suppssov1  8151  suppssov2  8152  suppss2  8154  suppssfv  8156  sniffsupp  9317  elfi2  9331  fifo  9349  en2other2  9933  finacn  9974  acndom2  9978  dfacacn  10066  kmlem11  10085  acncc  10364  axdc2lem  10372  1div0OLD  11811  elfzodif0  13700  expne0i  14031  incexc  15774  fprodn0f  15928  oddprm  16752  firest  17366  pfxchn  18547  chnind  18558  chnccat  18563  chnrev  18564  symgextf1lem  19366  pmtrmvd  19402  efgsp1  19683  efgredlem  19693  gsummpt1n0  19911  dprdfid  19965  dprdres  19976  dprd2da  19990  dmdprdsplit2lem  19993  ablfac1b  20018  ringelnzr  20473  isdomn4  20666  fidomndrnglem  20722  imadrhmcl  20747  sdrgacs  20751  cntzsdrg  20752  lvecinv  21085  lspsncmp  21088  lspsneq  21094  lspsneu  21095  lspdisjb  21098  lspexch  21101  lvecindp2  21111  cnflddiv  21372  uvcff  21763  frlmssuvc2  21767  frlmup2  21771  lindfrn  21793  f1lindf  21794  psrridm  21935  mplsubrg  21977  mplmon  22007  mplmonmul  22008  coe1tmmul  22236  dmatmul  22458  1marepvsma1  22544  mdetrsca2  22565  mdetrlin2  22568  mdetunilem5  22577  mdetunilem9  22581  maducoeval2  22601  gsummatr01lem3  22618  gsummatr01lem4  22619  gsummatr01  22620  cmpfi  23369  ptpjpre2  23541  alexsublem  24005  ptcmplem2  24014  divcn  24832  divcncf  25421  i1fmullem  25668  itg1addlem4  25673  itg1addlem5  25674  i1fmulc  25677  itg1mulc  25678  i1fres  25679  itg10a  25684  itg1climres  25688  mbfi1fseqlem4  25692  ellimc2  25851  dvcnp2  25894  dvcnp2OLD  25895  dvaddbr  25913  dvmulbr  25914  dvmulbrOLD  25915  dvcobr  25922  dvcobrOLD  25923  dvcjbr  25926  dvrec  25932  dvrecg  25950  dvcnvlem  25953  dvexp3  25955  dveflem  25956  ftc1lem6  26021  deg1n0ima  26067  ig1peu  26153  plyeq0lem  26188  dgrlem  26207  dgrlb  26214  coemulhi  26232  fta1  26289  aannenlem2  26310  tayl0  26342  taylthlem2  26355  taylthlem2OLD  26356  abelthlem7  26421  dcubic  26829  rlimcnp  26948  efrlim  26952  efrlimOLD  26953  muinv  27176  logexprlim  27209  lgslem1  27281  lgsqr  27335  lgseisenlem2  27360  lgseisenlem4  27362  lgseisen  27363  lgsquadlem1  27364  lgsquad2  27370  m1lgs  27372  dchrisum0re  27497  dchrisum0lema  27498  dchrisum0lem2  27502  dchrisum0lem3  27503  nnne0s  28350  uhgrn0  29158  upgrn0  29180  upgrex  29183  numedglnl  29235  upgrreslem  29395  isuvtx  29486  cusgrexilem2  29533  cusgrexi  29534  structtocusgr  29537  cusgrfilem2  29548  frgrhash2wsp  30425  1div0apr  30561  fmptunsnop  32796  disjdsct  32799  fxpsdrg  33275  elrgspnlem2  33343  elrgspnlem3  33344  domnprodn0  33375  isdrng4  33395  fracfld  33408  lindssn  33477  drngidl  33532  pidufd  33642  1arithufdlem3  33645  dfufd2  33649  zringidom  33650  zringfrac  33653  deg1prod  33682  ig1pmindeg  33701  psrmonmul  33733  assafld  33821  irngnzply1  33875  irngnminplynz  33896  constrsdrg  33959  signstfvneq0  34756  lfuhgr2  35341  cusgredgex  35344  loop1cycl  35359  subfacp1lem1  35401  circum  35896  neibastop1  36581  bj-xpnzexb  37236  bj-restn0b  37371  curf  37878  poimirlem2  37902  poimirlem24  37924  poimirlem25  37925  dvtan  37950  ftc1cnnc  37972  ftc1anclem3  37975  rrndstprj2  38111  lsat0cv  39438  lkreqN  39575  lkrlspeqN  39576  dochnel  41798  djhcvat42  41820  dochsnkr  41877  dochsnkr2cl  41879  lcfl6lem  41903  lcfl8b  41909  lcfrlem16  41963  lcfrlem25  41972  lcfrlem27  41974  lcfrlem33  41980  lcfrlem37  41984  mapdn0  42074  mapdpglem24  42109  mapdindp1  42125  mapdhval2  42131  hdmap1val2  42205  hdmapnzcl  42250  hdmap14lem1  42273  hdmap14lem4a  42276  hdmap14lem6  42278  hgmaprnlem1N  42301  hdmapip1  42321  hgmapvvlem1  42328  hgmapvvlem2  42329  aks6d1c5lem2  42537  resuppsinopn  42762  readvcot  42763  domnexpgn0cl  42922  prjspersym  42994  prjspreln0  42996  prjspvs  42997  dffltz  43021  aomclem2  43441  mpaaeu  43536  deg1mhm  43586  gneispace  44519  radcnvrat  44699  bccm1k  44727  disjf1o  45579  supminfxr2  45856  icoiccdif  45913  climrec  45992  climdivf  46001  lptre2pt  46027  0ellimcdiv  46036  limclner  46038  reclimc  46040  cnrefiisplem  46216  cncficcgt0  46275  fperdvper  46306  dvdivcncf  46314  dvnmul  46330  stoweidlem57  46444  dirkercncflem1  46490  fourierdlem24  46518  fourierdlem62  46555  fourierdlem66  46559  elaa2  46621  etransclem35  46656  etransclem47  46668  meadjiunlem  46852  ovnhoilem1  46988  hspmbllem1  47013  fmtnoprmfac1lem  47953  isubgruhgr  48257  isubgr0uhgr  48262  lindssnlvec  48875  logcxp0  48924