Theorem eldifsni 4766

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2932   ∖ cdif 3923  {csn 4601

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-v 3461  df-dif 3929  df-sn 4602

This theorem is referenced by:  eldifsnneq  4767  neldifsn  4768  suppssov1  8196  suppssov2  8197  suppss2  8199  suppssfv  8201  sniffsupp  9412  elfi2  9426  fifo  9444  en2other2  10023  finacn  10064  acndom2  10068  dfacacn  10156  kmlem11  10175  acncc  10454  axdc2lem  10462  1div0OLD  11897  expne0i  14112  incexc  15853  fprodn0f  16007  oddprm  16830  firest  17446  symgextf1lem  19401  pmtrmvd  19437  efgsp1  19718  efgredlem  19728  gsummpt1n0  19946  dprdfid  20000  dprdres  20011  dprd2da  20025  dmdprdsplit2lem  20028  ablfac1b  20053  ringelnzr  20483  isdomn4  20676  fidomndrnglem  20732  imadrhmcl  20757  sdrgacs  20761  cntzsdrg  20762  lvecinv  21074  lspsncmp  21077  lspsneq  21083  lspsneu  21084  lspdisjb  21087  lspexch  21090  lvecindp2  21100  cnflddiv  21363  uvcff  21751  frlmssuvc2  21755  frlmup2  21759  lindfrn  21781  f1lindf  21782  psrridm  21923  mplsubrg  21965  mplmon  21993  mplmonmul  21994  coe1tmmul  22214  dmatmul  22435  1marepvsma1  22521  mdetrsca2  22542  mdetrlin2  22545  mdetunilem5  22554  mdetunilem9  22558  maducoeval2  22578  gsummatr01lem3  22595  gsummatr01lem4  22596  gsummatr01  22597  cmpfi  23346  ptpjpre2  23518  alexsublem  23982  ptcmplem2  23991  divcn  24810  divcncf  25400  i1fmullem  25647  itg1addlem4  25652  itg1addlem5  25653  i1fmulc  25656  itg1mulc  25657  i1fres  25658  itg10a  25663  itg1climres  25667  mbfi1fseqlem4  25671  ellimc2  25830  dvcnp2  25873  dvcnp2OLD  25874  dvaddbr  25892  dvmulbr  25893  dvmulbrOLD  25894  dvcobr  25901  dvcobrOLD  25902  dvcjbr  25905  dvrec  25911  dvrecg  25929  dvcnvlem  25932  dvexp3  25934  dveflem  25935  ftc1lem6  26000  deg1n0ima  26046  ig1peu  26132  plyeq0lem  26167  dgrlem  26186  dgrlb  26193  coemulhi  26211  fta1  26268  aannenlem2  26289  tayl0  26321  taylthlem2  26334  taylthlem2OLD  26335  abelthlem7  26400  dcubic  26808  rlimcnp  26927  efrlim  26931  efrlimOLD  26932  muinv  27155  logexprlim  27188  lgslem1  27260  lgsqr  27314  lgseisenlem2  27339  lgseisenlem4  27341  lgseisen  27342  lgsquadlem1  27343  lgsquad2  27349  m1lgs  27351  dchrisum0re  27476  dchrisum0lema  27477  dchrisum0lem2  27481  dchrisum0lem3  27482  nnne0s  28281  uhgrn0  29046  upgrn0  29068  upgrex  29071  numedglnl  29123  upgrreslem  29283  isuvtx  29374  cusgrexilem2  29421  cusgrexi  29422  structtocusgr  29425  cusgrfilem2  29436  frgrhash2wsp  30313  1div0apr  30449  fmptunsnop  32677  disjdsct  32680  elfzodif0  32771  pfxchn  32989  chnind  32991  elrgspnlem2  33238  elrgspnlem3  33239  domnprodn0  33270  isdrng4  33289  fracfld  33302  lindssn  33393  drngidl  33448  pidufd  33558  1arithufdlem3  33561  dfufd2  33565  zringidom  33566  zringfrac  33569  ig1pmindeg  33611  assafld  33677  irngnzply1  33732  irngnminplynz  33746  constrsdrg  33809  signstfvneq0  34604  lfuhgr2  35141  cusgredgex  35144  loop1cycl  35159  subfacp1lem1  35201  circum  35696  neibastop1  36377  bj-xpnzexb  36979  bj-restn0b  37109  curf  37622  poimirlem2  37646  poimirlem24  37668  poimirlem25  37669  dvtan  37694  ftc1cnnc  37716  ftc1anclem3  37719  rrndstprj2  37855  lsat0cv  39051  lkreqN  39188  lkrlspeqN  39189  dochnel  41412  djhcvat42  41434  dochsnkr  41491  dochsnkr2cl  41493  lcfl6lem  41517  lcfl8b  41523  lcfrlem16  41577  lcfrlem25  41586  lcfrlem27  41588  lcfrlem33  41594  lcfrlem37  41598  mapdn0  41688  mapdpglem24  41723  mapdindp1  41739  mapdhval2  41745  hdmap1val2  41819  hdmapnzcl  41864  hdmap14lem1  41887  hdmap14lem4a  41890  hdmap14lem6  41892  hgmaprnlem1N  41915  hdmapip1  41935  hgmapvvlem1  41942  hgmapvvlem2  41943  aks6d1c5lem2  42151  resuppsinopn  42406  readvcot  42407  domnexpgn0cl  42546  prjspersym  42630  prjspreln0  42632  prjspvs  42633  dffltz  42657  aomclem2  43079  mpaaeu  43174  deg1mhm  43224  gneispace  44158  radcnvrat  44338  bccm1k  44366  disjf1o  45215  supminfxr2  45496  icoiccdif  45553  climrec  45632  climdivf  45641  lptre2pt  45669  0ellimcdiv  45678  limclner  45680  reclimc  45682  cnrefiisplem  45858  cncficcgt0  45917  fperdvper  45948  dvdivcncf  45956  dvnmul  45972  stoweidlem57  46086  dirkercncflem1  46132  fourierdlem24  46160  fourierdlem62  46197  fourierdlem66  46201  elaa2  46263  etransclem35  46298  etransclem47  46310  meadjiunlem  46494  ovnhoilem1  46630  hspmbllem1  46655  fmtnoprmfac1lem  47578  isubgruhgr  47881  isubgr0uhgr  47886  lindssnlvec  48462  logcxp0  48515