Theorem eldifsni 4683

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

Syntax hints:   → wi 4   ∈ wcel 2111   ≠ wne 2987   ∖ cdif 3878  {csn 4525

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-v 3443  df-dif 3884  df-sn 4526

This theorem is referenced by:  eldifsnneq  4684  neldifsn  4685  suppssov1  7845  suppss2  7847  suppssfv  7849  sniffsupp  8857  elfi2  8862  fifo  8880  en2other2  9420  finacn  9461  acndom2  9465  dfacacn  9552  kmlem11  9571  acncc  9851  axdc2lem  9859  1div0  11288  expne0i  13457  incexc  15184  fprodn0f  15337  oddprm  16137  firest  16698  symgextf1lem  18540  pmtrmvd  18576  efgsp1  18855  efgredlem  18865  gsummpt1n0  19078  dprdfid  19132  dprdres  19143  dprd2da  19157  dmdprdsplit2lem  19160  ablfac1b  19185  sdrgacs  19573  cntzsdrg  19574  lvecinv  19878  lspsncmp  19881  lspsneq  19887  lspsneu  19888  lspdisjb  19891  lspexch  19894  lvecindp2  19904  ringelnzr  20032  fidomndrnglem  20072  uvcff  20480  frlmssuvc2  20484  frlmup2  20488  lindfrn  20510  f1lindf  20511  psrridm  20642  mplsubrg  20678  mplmon  20703  mplmonmul  20704  coe1tmmul  20906  dmatmul  21102  1marepvsma1  21188  mdetrsca2  21209  mdetrlin2  21212  mdetunilem5  21221  mdetunilem9  21225  maducoeval2  21245  gsummatr01lem3  21262  gsummatr01lem4  21263  gsummatr01  21264  cmpfi  22013  ptpjpre2  22185  alexsublem  22649  ptcmplem2  22658  divcncf  24051  i1fmullem  24298  itg1addlem4  24303  itg1addlem5  24304  i1fmulc  24307  itg1mulc  24308  i1fres  24309  itg10a  24314  itg1climres  24318  mbfi1fseqlem4  24322  ellimc2  24480  dvcnp2  24523  dvaddbr  24541  dvmulbr  24542  dvcobr  24549  dvcjbr  24552  dvrec  24558  dvrecg  24576  dvcnvlem  24579  dvexp3  24581  dveflem  24582  ftc1lem6  24644  deg1n0ima  24690  ig1peu  24772  plyeq0lem  24807  dgrlem  24826  dgrlb  24833  coemulhi  24851  fta1  24904  aannenlem2  24925  tayl0  24957  taylthlem2  24969  abelthlem7  25033  dcubic  25432  rlimcnp  25551  efrlim  25555  muinv  25778  logexprlim  25809  lgslem1  25881  lgsqr  25935  lgseisenlem2  25960  lgseisenlem4  25962  lgseisen  25963  lgsquadlem1  25964  lgsquad2  25970  m1lgs  25972  dchrisum0re  26097  dchrisum0lema  26098  dchrisum0lem2  26102  dchrisum0lem3  26103  uhgrn0  26860  upgrn0  26882  upgrex  26885  numedglnl  26937  upgrreslem  27094  isuvtx  27185  cusgrexilem2  27232  cusgrexi  27233  structtocusgr  27236  cusgrfilem2  27246  frgrhash2wsp  28117  1div0apr  28253  disjdsct  30462  lindssn  30993  signstfvneq0  31952  lfuhgr2  32478  cusgredgex  32481  loop1cycl  32497  subfacp1lem1  32539  circum  33030  neibastop1  33820  bj-xpnzexb  34397  bj-restn0b  34506  curf  35035  poimirlem2  35059  poimirlem24  35081  poimirlem25  35082  dvtan  35107  ftc1cnnc  35129  ftc1anclem3  35132  rrndstprj2  35269  lsat0cv  36329  lkreqN  36466  lkrlspeqN  36467  dochnel  38689  djhcvat42  38711  dochsnkr  38768  dochsnkr2cl  38770  lcfl6lem  38794  lcfl8b  38800  lcfrlem16  38854  lcfrlem25  38863  lcfrlem27  38865  lcfrlem33  38871  lcfrlem37  38875  mapdn0  38965  mapdpglem24  39000  mapdindp1  39016  mapdhval2  39022  hdmap1val2  39096  hdmapnzcl  39141  hdmap14lem1  39164  hdmap14lem4a  39167  hdmap14lem6  39169  hgmaprnlem1N  39192  hdmapip1  39212  hgmapvvlem1  39219  hgmapvvlem2  39220  prjspersym  39601  prjspreln0  39603  prjspvs  39604  dffltz  39615  aomclem2  39999  mpaaeu  40094  deg1mhm  40151  gneispace  40837  radcnvrat  41018  bccm1k  41046  disjf1o  41818  supminfxr2  42108  icoiccdif  42161  climrec  42245  climdivf  42254  lptre2pt  42282  0ellimcdiv  42291  limclner  42293  reclimc  42295  cnrefiisplem  42471  cncficcgt0  42530  fperdvper  42561  dvdivcncf  42569  dvnmul  42585  stoweidlem57  42699  dirkercncflem1  42745  fourierdlem24  42773  fourierdlem62  42810  fourierdlem66  42814  elaa2  42876  etransclem35  42911  etransclem47  42923  meadjiunlem  43104  ovnhoilem1  43240  hspmbllem1  43265  fmtnoprmfac1lem  44081  lindssnlvec  44895  logcxp0  44949