Theorem eldifsni 4750

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925   ∖ cdif 3908  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3446  df-dif 3914  df-sn 4586

This theorem is referenced by:  eldifsnneq  4751  neldifsn  4752  suppssov1  8153  suppssov2  8154  suppss2  8156  suppssfv  8158  sniffsupp  9327  elfi2  9341  fifo  9359  en2other2  9938  finacn  9979  acndom2  9983  dfacacn  10071  kmlem11  10090  acncc  10369  axdc2lem  10377  1div0OLD  11814  expne0i  14035  incexc  15779  fprodn0f  15933  oddprm  16757  firest  17371  symgextf1lem  19334  pmtrmvd  19370  efgsp1  19651  efgredlem  19661  gsummpt1n0  19879  dprdfid  19933  dprdres  19944  dprd2da  19958  dmdprdsplit2lem  19961  ablfac1b  19986  ringelnzr  20443  isdomn4  20636  fidomndrnglem  20692  imadrhmcl  20717  sdrgacs  20721  cntzsdrg  20722  lvecinv  21055  lspsncmp  21058  lspsneq  21064  lspsneu  21065  lspdisjb  21068  lspexch  21071  lvecindp2  21081  cnflddiv  21342  uvcff  21733  frlmssuvc2  21737  frlmup2  21741  lindfrn  21763  f1lindf  21764  psrridm  21905  mplsubrg  21947  mplmon  21975  mplmonmul  21976  coe1tmmul  22196  dmatmul  22417  1marepvsma1  22503  mdetrsca2  22524  mdetrlin2  22527  mdetunilem5  22536  mdetunilem9  22540  maducoeval2  22560  gsummatr01lem3  22577  gsummatr01lem4  22578  gsummatr01  22579  cmpfi  23328  ptpjpre2  23500  alexsublem  23964  ptcmplem2  23973  divcn  24792  divcncf  25381  i1fmullem  25628  itg1addlem4  25633  itg1addlem5  25634  i1fmulc  25637  itg1mulc  25638  i1fres  25639  itg10a  25644  itg1climres  25648  mbfi1fseqlem4  25652  ellimc2  25811  dvcnp2  25854  dvcnp2OLD  25855  dvaddbr  25873  dvmulbr  25874  dvmulbrOLD  25875  dvcobr  25882  dvcobrOLD  25883  dvcjbr  25886  dvrec  25892  dvrecg  25910  dvcnvlem  25913  dvexp3  25915  dveflem  25916  ftc1lem6  25981  deg1n0ima  26027  ig1peu  26113  plyeq0lem  26148  dgrlem  26167  dgrlb  26174  coemulhi  26192  fta1  26249  aannenlem2  26270  tayl0  26302  taylthlem2  26315  taylthlem2OLD  26316  abelthlem7  26381  dcubic  26789  rlimcnp  26908  efrlim  26912  efrlimOLD  26913  muinv  27136  logexprlim  27169  lgslem1  27241  lgsqr  27295  lgseisenlem2  27320  lgseisenlem4  27322  lgseisen  27323  lgsquadlem1  27324  lgsquad2  27330  m1lgs  27332  dchrisum0re  27457  dchrisum0lema  27458  dchrisum0lem2  27462  dchrisum0lem3  27463  nnne0s  28269  uhgrn0  29047  upgrn0  29069  upgrex  29072  numedglnl  29124  upgrreslem  29284  isuvtx  29375  cusgrexilem2  29422  cusgrexi  29423  structtocusgr  29426  cusgrfilem2  29437  frgrhash2wsp  30311  1div0apr  30447  fmptunsnop  32673  disjdsct  32676  elfzodif0  32767  pfxchn  32981  chnind  32983  elrgspnlem2  33210  elrgspnlem3  33211  domnprodn0  33242  isdrng4  33261  fracfld  33274  lindssn  33342  drngidl  33397  pidufd  33507  1arithufdlem3  33510  dfufd2  33514  zringidom  33515  zringfrac  33518  ig1pmindeg  33560  assafld  33626  irngnzply1  33679  irngnminplynz  33695  constrsdrg  33758  signstfvneq0  34556  lfuhgr2  35099  cusgredgex  35102  loop1cycl  35117  subfacp1lem1  35159  circum  35654  neibastop1  36340  bj-xpnzexb  36942  bj-restn0b  37072  curf  37585  poimirlem2  37609  poimirlem24  37631  poimirlem25  37632  dvtan  37657  ftc1cnnc  37679  ftc1anclem3  37682  rrndstprj2  37818  lsat0cv  39019  lkreqN  39156  lkrlspeqN  39157  dochnel  41380  djhcvat42  41402  dochsnkr  41459  dochsnkr2cl  41461  lcfl6lem  41485  lcfl8b  41491  lcfrlem16  41545  lcfrlem25  41554  lcfrlem27  41556  lcfrlem33  41562  lcfrlem37  41566  mapdn0  41656  mapdpglem24  41691  mapdindp1  41707  mapdhval2  41713  hdmap1val2  41787  hdmapnzcl  41832  hdmap14lem1  41855  hdmap14lem4a  41858  hdmap14lem6  41860  hgmaprnlem1N  41883  hdmapip1  41903  hgmapvvlem1  41910  hgmapvvlem2  41911  aks6d1c5lem2  42119  resuppsinopn  42344  readvcot  42345  domnexpgn0cl  42504  prjspersym  42588  prjspreln0  42590  prjspvs  42591  dffltz  42615  aomclem2  43037  mpaaeu  43132  deg1mhm  43182  gneispace  44116  radcnvrat  44296  bccm1k  44324  disjf1o  45178  supminfxr2  45458  icoiccdif  45515  climrec  45594  climdivf  45603  lptre2pt  45631  0ellimcdiv  45640  limclner  45642  reclimc  45644  cnrefiisplem  45820  cncficcgt0  45879  fperdvper  45910  dvdivcncf  45918  dvnmul  45934  stoweidlem57  46048  dirkercncflem1  46094  fourierdlem24  46122  fourierdlem62  46159  fourierdlem66  46163  elaa2  46225  etransclem35  46260  etransclem47  46272  meadjiunlem  46456  ovnhoilem1  46592  hspmbllem1  46617  fmtnoprmfac1lem  47558  isubgruhgr  47861  isubgr0uhgr  47866  lindssnlvec  48468  logcxp0  48517