Theorem eldifsni 4720

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2942   ∖ cdif 3880  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-v 3424  df-dif 3886  df-sn 4559

This theorem is referenced by:  eldifsnneq  4721  neldifsn  4722  suppssov1  7985  suppss2  7987  suppssfv  7989  sniffsupp  9089  elfi2  9103  fifo  9121  en2other2  9696  finacn  9737  acndom2  9741  dfacacn  9828  kmlem11  9847  acncc  10127  axdc2lem  10135  1div0  11564  expne0i  13743  incexc  15477  fprodn0f  15629  oddprm  16439  firest  17060  symgextf1lem  18943  pmtrmvd  18979  efgsp1  19258  efgredlem  19268  gsummpt1n0  19481  dprdfid  19535  dprdres  19546  dprd2da  19560  dmdprdsplit2lem  19563  ablfac1b  19588  sdrgacs  19984  cntzsdrg  19985  lvecinv  20290  lspsncmp  20293  lspsneq  20299  lspsneu  20300  lspdisjb  20303  lspexch  20306  lvecindp2  20316  ringelnzr  20450  fidomndrnglem  20491  uvcff  20908  frlmssuvc2  20912  frlmup2  20916  lindfrn  20938  f1lindf  20939  psrridm  21083  mplsubrg  21121  mplmon  21146  mplmonmul  21147  coe1tmmul  21358  dmatmul  21554  1marepvsma1  21640  mdetrsca2  21661  mdetrlin2  21664  mdetunilem5  21673  mdetunilem9  21677  maducoeval2  21697  gsummatr01lem3  21714  gsummatr01lem4  21715  gsummatr01  21716  cmpfi  22467  ptpjpre2  22639  alexsublem  23103  ptcmplem2  23112  divcncf  24516  i1fmullem  24763  itg1addlem4  24768  itg1addlem4OLD  24769  itg1addlem5  24770  i1fmulc  24773  itg1mulc  24774  i1fres  24775  itg10a  24780  itg1climres  24784  mbfi1fseqlem4  24788  ellimc2  24946  dvcnp2  24989  dvaddbr  25007  dvmulbr  25008  dvcobr  25015  dvcjbr  25018  dvrec  25024  dvrecg  25042  dvcnvlem  25045  dvexp3  25047  dveflem  25048  ftc1lem6  25110  deg1n0ima  25159  ig1peu  25241  plyeq0lem  25276  dgrlem  25295  dgrlb  25302  coemulhi  25320  fta1  25373  aannenlem2  25394  tayl0  25426  taylthlem2  25438  abelthlem7  25502  dcubic  25901  rlimcnp  26020  efrlim  26024  muinv  26247  logexprlim  26278  lgslem1  26350  lgsqr  26404  lgseisenlem2  26429  lgseisenlem4  26431  lgseisen  26432  lgsquadlem1  26433  lgsquad2  26439  m1lgs  26441  dchrisum0re  26566  dchrisum0lema  26567  dchrisum0lem2  26571  dchrisum0lem3  26572  uhgrn0  27340  upgrn0  27362  upgrex  27365  numedglnl  27417  upgrreslem  27574  isuvtx  27665  cusgrexilem2  27712  cusgrexi  27713  structtocusgr  27716  cusgrfilem2  27726  frgrhash2wsp  28597  1div0apr  28733  disjdsct  30937  lindssn  31475  signstfvneq0  32451  lfuhgr2  32980  cusgredgex  32983  loop1cycl  32999  subfacp1lem1  33041  circum  33532  neibastop1  34475  bj-xpnzexb  35078  bj-restn0b  35189  curf  35682  poimirlem2  35706  poimirlem24  35728  poimirlem25  35729  dvtan  35754  ftc1cnnc  35776  ftc1anclem3  35779  rrndstprj2  35916  lsat0cv  36974  lkreqN  37111  lkrlspeqN  37112  dochnel  39334  djhcvat42  39356  dochsnkr  39413  dochsnkr2cl  39415  lcfl6lem  39439  lcfl8b  39445  lcfrlem16  39499  lcfrlem25  39508  lcfrlem27  39510  lcfrlem33  39516  lcfrlem37  39520  mapdn0  39610  mapdpglem24  39645  mapdindp1  39661  mapdhval2  39667  hdmap1val2  39741  hdmapnzcl  39786  hdmap14lem1  39809  hdmap14lem4a  39812  hdmap14lem6  39814  hgmaprnlem1N  39837  hdmapip1  39857  hgmapvvlem1  39864  hgmapvvlem2  39865  isdomn4  40100  prjspersym  40367  prjspreln0  40369  prjspvs  40370  dffltz  40387  aomclem2  40796  mpaaeu  40891  deg1mhm  40948  gneispace  41633  radcnvrat  41821  bccm1k  41849  disjf1o  42618  supminfxr2  42899  icoiccdif  42952  climrec  43034  climdivf  43043  lptre2pt  43071  0ellimcdiv  43080  limclner  43082  reclimc  43084  cnrefiisplem  43260  cncficcgt0  43319  fperdvper  43350  dvdivcncf  43358  dvnmul  43374  stoweidlem57  43488  dirkercncflem1  43534  fourierdlem24  43562  fourierdlem62  43599  fourierdlem66  43603  elaa2  43665  etransclem35  43700  etransclem47  43712  meadjiunlem  43893  ovnhoilem1  44029  hspmbllem1  44054  fmtnoprmfac1lem  44904  lindssnlvec  45715  logcxp0  45769