Theorem eldifsni 4747

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933   ∖ cdif 3899  {csn 4581

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3443  df-dif 3905  df-sn 4582

This theorem is referenced by:  eldifsnneq  4748  neldifsn  4749  suppssov1  8141  suppssov2  8142  suppss2  8144  suppssfv  8146  sniffsupp  9307  elfi2  9321  fifo  9339  en2other2  9923  finacn  9964  acndom2  9968  dfacacn  10056  kmlem11  10075  acncc  10354  axdc2lem  10362  1div0OLD  11801  elfzodif0  13690  expne0i  14021  incexc  15764  fprodn0f  15918  oddprm  16742  firest  17356  pfxchn  18537  chnind  18548  chnccat  18553  chnrev  18554  symgextf1lem  19353  pmtrmvd  19389  efgsp1  19670  efgredlem  19680  gsummpt1n0  19898  dprdfid  19952  dprdres  19963  dprd2da  19977  dmdprdsplit2lem  19980  ablfac1b  20005  ringelnzr  20460  isdomn4  20653  fidomndrnglem  20709  imadrhmcl  20734  sdrgacs  20738  cntzsdrg  20739  lvecinv  21072  lspsncmp  21075  lspsneq  21081  lspsneu  21082  lspdisjb  21085  lspexch  21088  lvecindp2  21098  cnflddiv  21359  uvcff  21750  frlmssuvc2  21754  frlmup2  21758  lindfrn  21780  f1lindf  21781  psrridm  21922  mplsubrg  21964  mplmon  21994  mplmonmul  21995  coe1tmmul  22223  dmatmul  22445  1marepvsma1  22531  mdetrsca2  22552  mdetrlin2  22555  mdetunilem5  22564  mdetunilem9  22568  maducoeval2  22588  gsummatr01lem3  22605  gsummatr01lem4  22606  gsummatr01  22607  cmpfi  23356  ptpjpre2  23528  alexsublem  23992  ptcmplem2  24001  divcn  24819  divcncf  25408  i1fmullem  25655  itg1addlem4  25660  itg1addlem5  25661  i1fmulc  25664  itg1mulc  25665  i1fres  25666  itg10a  25671  itg1climres  25675  mbfi1fseqlem4  25679  ellimc2  25838  dvcnp2  25881  dvcnp2OLD  25882  dvaddbr  25900  dvmulbr  25901  dvmulbrOLD  25902  dvcobr  25909  dvcobrOLD  25910  dvcjbr  25913  dvrec  25919  dvrecg  25937  dvcnvlem  25940  dvexp3  25942  dveflem  25943  ftc1lem6  26008  deg1n0ima  26054  ig1peu  26140  plyeq0lem  26175  dgrlem  26194  dgrlb  26201  coemulhi  26219  fta1  26276  aannenlem2  26297  tayl0  26329  taylthlem2  26342  taylthlem2OLD  26343  abelthlem7  26408  dcubic  26816  rlimcnp  26935  efrlim  26939  efrlimOLD  26940  muinv  27163  logexprlim  27196  lgslem1  27268  lgsqr  27322  lgseisenlem2  27347  lgseisenlem4  27349  lgseisen  27350  lgsquadlem1  27351  lgsquad2  27357  m1lgs  27359  dchrisum0re  27484  dchrisum0lema  27485  dchrisum0lem2  27489  dchrisum0lem3  27490  nnne0s  28337  uhgrn0  29144  upgrn0  29166  upgrex  29169  numedglnl  29221  upgrreslem  29381  isuvtx  29472  cusgrexilem2  29519  cusgrexi  29520  structtocusgr  29523  cusgrfilem2  29534  frgrhash2wsp  30411  1div0apr  30547  fmptunsnop  32781  disjdsct  32784  fxpsdrg  33259  elrgspnlem2  33327  elrgspnlem3  33328  domnprodn0  33359  isdrng4  33379  fracfld  33392  lindssn  33461  drngidl  33516  pidufd  33626  1arithufdlem3  33629  dfufd2  33633  zringidom  33634  zringfrac  33637  deg1prod  33666  ig1pmindeg  33685  assafld  33796  irngnzply1  33850  irngnminplynz  33871  constrsdrg  33934  signstfvneq0  34731  lfuhgr2  35315  cusgredgex  35318  loop1cycl  35333  subfacp1lem1  35375  circum  35870  neibastop1  36555  bj-xpnzexb  37164  bj-restn0b  37298  curf  37801  poimirlem2  37825  poimirlem24  37847  poimirlem25  37848  dvtan  37873  ftc1cnnc  37895  ftc1anclem3  37898  rrndstprj2  38034  lsat0cv  39361  lkreqN  39498  lkrlspeqN  39499  dochnel  41721  djhcvat42  41743  dochsnkr  41800  dochsnkr2cl  41802  lcfl6lem  41826  lcfl8b  41832  lcfrlem16  41886  lcfrlem25  41895  lcfrlem27  41897  lcfrlem33  41903  lcfrlem37  41907  mapdn0  41997  mapdpglem24  42032  mapdindp1  42048  mapdhval2  42054  hdmap1val2  42128  hdmapnzcl  42173  hdmap14lem1  42196  hdmap14lem4a  42199  hdmap14lem6  42201  hgmaprnlem1N  42224  hdmapip1  42244  hgmapvvlem1  42251  hgmapvvlem2  42252  aks6d1c5lem2  42460  resuppsinopn  42685  readvcot  42686  domnexpgn0cl  42845  prjspersym  42917  prjspreln0  42919  prjspvs  42920  dffltz  42944  aomclem2  43364  mpaaeu  43459  deg1mhm  43509  gneispace  44442  radcnvrat  44622  bccm1k  44650  disjf1o  45502  supminfxr2  45780  icoiccdif  45837  climrec  45916  climdivf  45925  lptre2pt  45951  0ellimcdiv  45960  limclner  45962  reclimc  45964  cnrefiisplem  46140  cncficcgt0  46199  fperdvper  46230  dvdivcncf  46238  dvnmul  46254  stoweidlem57  46368  dirkercncflem1  46414  fourierdlem24  46442  fourierdlem62  46479  fourierdlem66  46483  elaa2  46545  etransclem35  46580  etransclem47  46592  meadjiunlem  46776  ovnhoilem1  46912  hspmbllem1  46937  fmtnoprmfac1lem  47877  isubgruhgr  48181  isubgr0uhgr  48186  lindssnlvec  48799  logcxp0  48848