Theorem eldifsni 4725

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2930   ∖ cdif 3882  {csn 4557

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ne 2931  df-v 3429  df-dif 3888  df-sn 4558

This theorem is referenced by:  eldifsnneq  4726  neldifsn  4727  suppssov1  8136  suppssov2  8137  suppss2  8139  suppssfv  8141  sniffsupp  9302  elfi2  9316  fifo  9334  en2other2  9920  finacn  9961  acndom2  9965  dfacacn  10053  kmlem11  10072  acncc  10351  axdc2lem  10359  1div0OLD  11799  elfzodif0  13714  expne0i  14045  incexc  15791  fprodn0f  15945  oddprm  16770  firest  17384  pfxchn  18565  chnind  18576  chnccat  18581  chnrev  18582  symgextf1lem  19384  pmtrmvd  19420  efgsp1  19701  efgredlem  19711  gsummpt1n0  19929  dprdfid  19983  dprdres  19994  dprd2da  20008  dmdprdsplit2lem  20011  ablfac1b  20036  ringelnzr  20489  isdomn4  20682  fidomndrnglem  20738  imadrhmcl  20763  sdrgacs  20767  cntzsdrg  20768  lvecinv  21100  lspsncmp  21103  lspsneq  21109  lspsneu  21110  lspdisjb  21113  lspexch  21116  lvecindp2  21126  cnflddiv  21371  uvcff  21760  frlmssuvc2  21764  frlmup2  21768  lindfrn  21790  f1lindf  21791  psrridm  21930  mplsubrg  21972  mplmon  22002  mplmonmul  22003  coe1tmmul  22230  dmatmul  22450  1marepvsma1  22536  mdetrsca2  22557  mdetrlin2  22560  mdetunilem5  22569  mdetunilem9  22573  maducoeval2  22593  gsummatr01lem3  22610  gsummatr01lem4  22611  gsummatr01  22612  cmpfi  23361  ptpjpre2  23533  alexsublem  23997  ptcmplem2  24006  divcn  24823  divcncf  25402  i1fmullem  25649  itg1addlem4  25654  itg1addlem5  25655  i1fmulc  25658  itg1mulc  25659  i1fres  25660  itg10a  25665  itg1climres  25669  mbfi1fseqlem4  25673  ellimc2  25832  dvcnp2  25875  dvaddbr  25893  dvmulbr  25894  dvcobr  25901  dvcjbr  25904  dvrec  25910  dvrecg  25928  dvcnvlem  25931  dvexp3  25933  dveflem  25934  ftc1lem6  25996  deg1n0ima  26042  ig1peu  26128  plyeq0lem  26163  dgrlem  26182  dgrlb  26189  coemulhi  26207  fta1  26262  aannenlem2  26283  tayl0  26315  taylthlem2  26327  abelthlem7  26391  dcubic  26798  rlimcnp  26917  efrlim  26921  muinv  27144  logexprlim  27176  lgslem1  27248  lgsqr  27302  lgseisenlem2  27327  lgseisenlem4  27329  lgseisen  27330  lgsquadlem1  27331  lgsquad2  27337  m1lgs  27339  dchrisum0re  27464  dchrisum0lema  27465  dchrisum0lem2  27469  dchrisum0lem3  27470  nnne0s  28317  uhgrn0  29124  upgrn0  29146  upgrex  29149  numedglnl  29201  upgrreslem  29361  isuvtx  29452  cusgrexilem2  29499  cusgrexi  29500  structtocusgr  29503  cusgrfilem2  29513  frgrhash2wsp  30390  1div0apr  30526  fmptunsnop  32761  disjdsct  32764  fxpsdrg  33224  elrgspnlem2  33292  elrgspnlem3  33293  domnprodn0  33324  isdrng4  33344  fracfld  33357  lindssn  33426  drngidl  33481  pidufd  33591  1arithufdlem3  33594  dfufd2  33598  zringidom  33599  zringfrac  33602  deg1prod  33631  ig1pmindeg  33650  psrmonmul  33682  assafld  33769  irngnzply1  33823  irngnminplynz  33844  constrsdrg  33907  signstfvneq0  34704  lfuhgr2  35289  cusgredgex  35292  loop1cycl  35307  subfacp1lem1  35349  circum  35844  neibastop1  36529  bj-xpnzexb  37256  bj-restn0b  37391  curf  37907  poimirlem2  37931  poimirlem24  37953  poimirlem25  37954  dvtan  37979  ftc1cnnc  38001  ftc1anclem3  38004  rrndstprj2  38140  lsat0cv  39467  lkreqN  39604  lkrlspeqN  39605  dochnel  41827  djhcvat42  41849  dochsnkr  41906  dochsnkr2cl  41908  lcfl6lem  41932  lcfl8b  41938  lcfrlem16  41992  lcfrlem25  42001  lcfrlem27  42003  lcfrlem33  42009  lcfrlem37  42013  mapdn0  42103  mapdpglem24  42138  mapdindp1  42154  mapdhval2  42160  hdmap1val2  42234  hdmapnzcl  42279  hdmap14lem1  42302  hdmap14lem4a  42305  hdmap14lem6  42307  hgmaprnlem1N  42330  hdmapip1  42350  hgmapvvlem1  42357  hgmapvvlem2  42358  aks6d1c5lem2  42565  resuppsinopn  42783  readvcot  42784  domnexpgn0cl  42956  prjspersym  43028  prjspreln0  43030  prjspvs  43031  dffltz  43055  aomclem2  43471  mpaaeu  43566  deg1mhm  43616  gneispace  44549  radcnvrat  44729  bccm1k  44757  disjf1o  45609  supminfxr2  45885  icoiccdif  45942  climrec  46021  climdivf  46030  lptre2pt  46056  0ellimcdiv  46065  limclner  46067  reclimc  46069  cnrefiisplem  46245  cncficcgt0  46304  fperdvper  46335  dvdivcncf  46343  dvnmul  46359  stoweidlem57  46473  dirkercncflem1  46519  fourierdlem24  46547  fourierdlem62  46584  fourierdlem66  46588  elaa2  46650  etransclem35  46685  etransclem47  46697  meadjiunlem  46881  ovnhoilem1  47017  hspmbllem1  47042  fmtnoprmfac1lem  48015  isubgruhgr  48332  isubgr0uhgr  48337  lindssnlvec  48950  logcxp0  48999