Theorem eldifsni 4760

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

Syntax hints:   → wi 4   ∈ wcel 2149   ≠ wne 2964   ∖ cdif 3908  {csn 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-v 3463  df-dif 3914  df-sn 4593

This theorem is referenced by:  eldifsnneq  4761  neldifsn  4762  suppssov1  8193  suppssov2  8194  suppss2  8196  suppssfv  8198  sniffsupp  9360  elfi2  9374  fifo  9392  en2other2  9993  finacn  10034  acndom2  10038  dfacacn  10125  kmlem11  10144  acncc  10424  axdc2lem  10432  elfzodif0  13799  expne0i  14130  incexc  15891  fprodn0f  16045  oddprm  16870  firest  17485  pfxchn  18666  chnind  18677  chnccat  18682  chnrev  18683  symgextf1lem  19490  pmtrmvd  19526  efgsp1  19807  efgredlem  19817  gsummpt1n0  20035  dprdfid  20089  dprdres  20100  dprd2da  20114  dmdprdsplit2lem  20117  ablfac1b  20142  ringelnzr  20607  isdomn4  20800  fidomndrnglem  20854  imadrhmcl  20878  sdrgacs  20882  cntzsdrg  20883  lvecinv  21215  lspsncmp  21218  lspsneq  21224  lspsneu  21225  lspdisjb  21228  lspexch  21231  lvecindp2  21241  cnflddiv  21521  uvcff  21910  frlmssuvc2  21914  frlmup2  21918  lindfrn  21940  f1lindf  21941  psrridm  22081  mplsubrg  22123  mplmon  22155  mplmonmul  22156  coe1tmmul  22407  dmatmul  22623  1marepvsma1  22709  mdetrsca2  22730  mdetrlin2  22733  mdetunilem5  22742  mdetunilem9  22746  maducoeval2  22766  gsummatr01lem3  22783  gsummatr01lem4  22784  gsummatr01  22785  cmpfi  23534  ptpjpre2  23706  alexsublem  24170  ptcmplem2  24179  divcn  24996  divcncf  25575  i1fmullem  25822  itg1addlem4  25827  itg1addlem5  25828  i1fmulc  25831  itg1mulc  25832  i1fres  25833  itg10a  25838  itg1climres  25842  mbfi1fseqlem4  25846  ellimc2  26005  dvcnp2  26048  dvaddbr  26066  dvmulbr  26067  dvcobr  26074  dvcjbr  26077  dvrec  26083  dvrecg  26101  dvcnvlem  26104  dvexp3  26106  dveflem  26107  ftc1lem6  26169  deg1n0ima  26215  ig1peu  26301  plyeq0lem  26336  dgrlem  26355  dgrlb  26362  coemulhi  26380  fta1  26438  aannenlem2  26459  tayl0  26491  taylthlem2  26503  abelthlem7  26567  dcubic  26977  rlimcnp  27096  efrlim  27100  muinv  27323  logexprlim  27355  lgslem1  27427  lgsqr  27481  lgseisenlem2  27506  lgseisenlem4  27508  lgseisen  27509  lgsquadlem1  27510  lgsquad2  27516  m1lgs  27518  dchrisum0re  27643  dchrisum0lema  27644  dchrisum0lem2  27648  dchrisum0lem3  27649  nnne0s  28496  uhgrn0  29358  upgrn0  29380  upgrex  29383  numedglnl  29435  upgrreslem  29595  isuvtx  29686  cusgrexilem2  29733  cusgrexi  29734  structtocusgr  29737  cusgrfilem2  29747  frgrhash2wsp  30624  1div0apr  30760  fmptunsnop  32986  disjdsct  32989  fxpsdrg  33436  elrgspnlem2  33504  elrgspnlem3  33505  domnprodn0  33539  isdrng4  33559  fracfld  33572  lindssn  33635  drngidl  33685  pidufd  33778  1arithufdlem3  33781  dfufd2  33785  zringidom  33786  zringfrac  33789  deg1prod  33818  ig1pmindeg  33837  psrmonmul  33885  assafld  33972  irngnzply1  34026  irngnminplynz  34047  constrsdrg  34110  signstfvneq0  34904  lfuhgr2  35544  cusgredgex  35547  loop1cycl  35562  subfacp1lem1  35604  circum  36099  neibastop1  36793  bj-xpnzexb  37520  bj-restn0b  37656  curf  38172  poimirlem2  38196  poimirlem24  38218  poimirlem25  38219  dvtan  38244  ftc1cnnc  38266  ftc1anclem3  38269  rrndstprj2  38405  lsat0cv  39732  lkreqN  39869  lkrlspeqN  39870  dochnel  42092  djhcvat42  42114  dochsnkr  42171  dochsnkr2cl  42173  lcfl6lem  42197  lcfl8b  42203  lcfrlem16  42257  lcfrlem25  42266  lcfrlem27  42268  lcfrlem33  42274  lcfrlem37  42278  mapdn0  42368  mapdpglem24  42403  mapdindp1  42419  mapdhval2  42425  hdmap1val2  42499  hdmapnzcl  42544  hdmap14lem1  42567  hdmap14lem4a  42570  hdmap14lem6  42572  hgmaprnlem1N  42595  hdmapip1  42615  hgmapvvlem1  42622  hgmapvvlem2  42623  aks6d1c5lem2  42830  resuppsinopn  43049  readvcot  43050  domnexpgn0cl  43218  prjspersym  43266  prjspreln0  43268  prjspvs  43269  dffltz  43293  aomclem2  43709  mpaaeu  43804  deg1mhm  43854  gneispace  44787  radcnvrat  44951  bccm1k  44979  disjf1o  45836  supminfxr2  46110  icoiccdif  46167  climrec  46246  climdivf  46255  lptre2pt  46281  0ellimcdiv  46290  limclner  46292  reclimc  46294  cnrefiisplem  46470  cncficcgt0  46529  fperdvper  46560  dvdivcncf  46568  dvnmul  46584  stoweidlem57  46698  dirkercncflem1  46744  fourierdlem24  46772  fourierdlem62  46809  fourierdlem66  46813  elaa2  46875  etransclem35  46910  etransclem47  46922  meadjiunlem  47106  ovnhoilem1  47242  hspmbllem1  47267  fmtnoprmfac1lem  48240  isubgruhgr  48557  isubgr0uhgr  48562  lindssnlvec  49186  logcxp0  49235