Theorem eldifsni 4688

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2935   ∖ cdif 3850  {csn 4526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-ne 2936  df-v 3402  df-dif 3856  df-sn 4527

This theorem is referenced by:  eldifsnneq  4689  neldifsn  4690  suppssov1  7906  suppss2  7908  suppssfv  7910  sniffsupp  8950  elfi2  8964  fifo  8982  en2other2  9522  finacn  9563  acndom2  9567  dfacacn  9654  kmlem11  9673  acncc  9953  axdc2lem  9961  1div0  11390  expne0i  13566  incexc  15298  fprodn0f  15450  oddprm  16260  firest  16822  symgextf1lem  18679  pmtrmvd  18715  efgsp1  18994  efgredlem  19004  gsummpt1n0  19217  dprdfid  19271  dprdres  19282  dprd2da  19296  dmdprdsplit2lem  19299  ablfac1b  19324  sdrgacs  19712  cntzsdrg  19713  lvecinv  20017  lspsncmp  20020  lspsneq  20026  lspsneu  20027  lspdisjb  20030  lspexch  20033  lvecindp2  20043  ringelnzr  20171  fidomndrnglem  20211  uvcff  20620  frlmssuvc2  20624  frlmup2  20628  lindfrn  20650  f1lindf  20651  psrridm  20796  mplsubrg  20834  mplmon  20859  mplmonmul  20860  coe1tmmul  21065  dmatmul  21261  1marepvsma1  21347  mdetrsca2  21368  mdetrlin2  21371  mdetunilem5  21380  mdetunilem9  21384  maducoeval2  21404  gsummatr01lem3  21421  gsummatr01lem4  21422  gsummatr01  21423  cmpfi  22172  ptpjpre2  22344  alexsublem  22808  ptcmplem2  22817  divcncf  24212  i1fmullem  24459  itg1addlem4  24464  itg1addlem4OLD  24465  itg1addlem5  24466  i1fmulc  24469  itg1mulc  24470  i1fres  24471  itg10a  24476  itg1climres  24480  mbfi1fseqlem4  24484  ellimc2  24642  dvcnp2  24685  dvaddbr  24703  dvmulbr  24704  dvcobr  24711  dvcjbr  24714  dvrec  24720  dvrecg  24738  dvcnvlem  24741  dvexp3  24743  dveflem  24744  ftc1lem6  24806  deg1n0ima  24855  ig1peu  24937  plyeq0lem  24972  dgrlem  24991  dgrlb  24998  coemulhi  25016  fta1  25069  aannenlem2  25090  tayl0  25122  taylthlem2  25134  abelthlem7  25198  dcubic  25597  rlimcnp  25716  efrlim  25720  muinv  25943  logexprlim  25974  lgslem1  26046  lgsqr  26100  lgseisenlem2  26125  lgseisenlem4  26127  lgseisen  26128  lgsquadlem1  26129  lgsquad2  26135  m1lgs  26137  dchrisum0re  26262  dchrisum0lema  26263  dchrisum0lem2  26267  dchrisum0lem3  26268  uhgrn0  27025  upgrn0  27047  upgrex  27050  numedglnl  27102  upgrreslem  27259  isuvtx  27350  cusgrexilem2  27397  cusgrexi  27398  structtocusgr  27401  cusgrfilem2  27411  frgrhash2wsp  28282  1div0apr  28418  disjdsct  30623  lindssn  31158  signstfvneq0  32134  lfuhgr2  32664  cusgredgex  32667  loop1cycl  32683  subfacp1lem1  32725  circum  33216  neibastop1  34204  bj-xpnzexb  34807  bj-restn0b  34916  curf  35411  poimirlem2  35435  poimirlem24  35457  poimirlem25  35458  dvtan  35483  ftc1cnnc  35505  ftc1anclem3  35508  rrndstprj2  35645  lsat0cv  36703  lkreqN  36840  lkrlspeqN  36841  dochnel  39063  djhcvat42  39085  dochsnkr  39142  dochsnkr2cl  39144  lcfl6lem  39168  lcfl8b  39174  lcfrlem16  39228  lcfrlem25  39237  lcfrlem27  39239  lcfrlem33  39245  lcfrlem37  39249  mapdn0  39339  mapdpglem24  39374  mapdindp1  39390  mapdhval2  39396  hdmap1val2  39470  hdmapnzcl  39515  hdmap14lem1  39538  hdmap14lem4a  39541  hdmap14lem6  39543  hgmaprnlem1N  39566  hdmapip1  39586  hgmapvvlem1  39593  hgmapvvlem2  39594  isdomn4  39804  prjspersym  40064  prjspreln0  40066  prjspvs  40067  dffltz  40084  aomclem2  40493  mpaaeu  40588  deg1mhm  40645  gneispace  41331  radcnvrat  41511  bccm1k  41539  disjf1o  42308  supminfxr2  42590  icoiccdif  42643  climrec  42727  climdivf  42736  lptre2pt  42764  0ellimcdiv  42773  limclner  42775  reclimc  42777  cnrefiisplem  42953  cncficcgt0  43012  fperdvper  43043  dvdivcncf  43051  dvnmul  43067  stoweidlem57  43181  dirkercncflem1  43227  fourierdlem24  43255  fourierdlem62  43292  fourierdlem66  43296  elaa2  43358  etransclem35  43393  etransclem47  43405  meadjiunlem  43586  ovnhoilem1  43722  hspmbllem1  43747  fmtnoprmfac1lem  44598  lindssnlvec  45409  logcxp0  45463