Theorem eldifsni 4724

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

Syntax hints:   → wi 4   ∈ wcel 2107   ≠ wne 2944   ∖ cdif 3885  {csn 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-v 3435  df-dif 3891  df-sn 4563

This theorem is referenced by:  eldifsnneq  4725  neldifsn  4726  suppssov1  8023  suppss2  8025  suppssfv  8027  sniffsupp  9168  elfi2  9182  fifo  9200  en2other2  9774  finacn  9815  acndom2  9819  dfacacn  9906  kmlem11  9925  acncc  10205  axdc2lem  10213  1div0  11643  expne0i  13824  incexc  15558  fprodn0f  15710  oddprm  16520  firest  17152  symgextf1lem  19037  pmtrmvd  19073  efgsp1  19352  efgredlem  19362  gsummpt1n0  19575  dprdfid  19629  dprdres  19640  dprd2da  19654  dmdprdsplit2lem  19657  ablfac1b  19682  sdrgacs  20078  cntzsdrg  20079  lvecinv  20384  lspsncmp  20387  lspsneq  20393  lspsneu  20394  lspdisjb  20397  lspexch  20400  lvecindp2  20410  ringelnzr  20546  fidomndrnglem  20587  uvcff  21007  frlmssuvc2  21011  frlmup2  21015  lindfrn  21037  f1lindf  21038  psrridm  21182  mplsubrg  21220  mplmon  21245  mplmonmul  21246  coe1tmmul  21457  dmatmul  21655  1marepvsma1  21741  mdetrsca2  21762  mdetrlin2  21765  mdetunilem5  21774  mdetunilem9  21778  maducoeval2  21798  gsummatr01lem3  21815  gsummatr01lem4  21816  gsummatr01  21817  cmpfi  22568  ptpjpre2  22740  alexsublem  23204  ptcmplem2  23213  divcncf  24620  i1fmullem  24867  itg1addlem4  24872  itg1addlem4OLD  24873  itg1addlem5  24874  i1fmulc  24877  itg1mulc  24878  i1fres  24879  itg10a  24884  itg1climres  24888  mbfi1fseqlem4  24892  ellimc2  25050  dvcnp2  25093  dvaddbr  25111  dvmulbr  25112  dvcobr  25119  dvcjbr  25122  dvrec  25128  dvrecg  25146  dvcnvlem  25149  dvexp3  25151  dveflem  25152  ftc1lem6  25214  deg1n0ima  25263  ig1peu  25345  plyeq0lem  25380  dgrlem  25399  dgrlb  25406  coemulhi  25424  fta1  25477  aannenlem2  25498  tayl0  25530  taylthlem2  25542  abelthlem7  25606  dcubic  26005  rlimcnp  26124  efrlim  26128  muinv  26351  logexprlim  26382  lgslem1  26454  lgsqr  26508  lgseisenlem2  26533  lgseisenlem4  26535  lgseisen  26536  lgsquadlem1  26537  lgsquad2  26543  m1lgs  26545  dchrisum0re  26670  dchrisum0lema  26671  dchrisum0lem2  26675  dchrisum0lem3  26676  uhgrn0  27446  upgrn0  27468  upgrex  27471  numedglnl  27523  upgrreslem  27680  isuvtx  27771  cusgrexilem2  27818  cusgrexi  27819  structtocusgr  27822  cusgrfilem2  27832  frgrhash2wsp  28705  1div0apr  28841  disjdsct  31044  lindssn  31582  signstfvneq0  32560  lfuhgr2  33089  cusgredgex  33092  loop1cycl  33108  subfacp1lem1  33150  circum  33641  neibastop1  34557  bj-xpnzexb  35160  bj-restn0b  35271  curf  35764  poimirlem2  35788  poimirlem24  35810  poimirlem25  35811  dvtan  35836  ftc1cnnc  35858  ftc1anclem3  35861  rrndstprj2  35998  lsat0cv  37054  lkreqN  37191  lkrlspeqN  37192  dochnel  39414  djhcvat42  39436  dochsnkr  39493  dochsnkr2cl  39495  lcfl6lem  39519  lcfl8b  39525  lcfrlem16  39579  lcfrlem25  39588  lcfrlem27  39590  lcfrlem33  39596  lcfrlem37  39600  mapdn0  39690  mapdpglem24  39725  mapdindp1  39741  mapdhval2  39747  hdmap1val2  39821  hdmapnzcl  39866  hdmap14lem1  39889  hdmap14lem4a  39892  hdmap14lem6  39894  hgmaprnlem1N  39917  hdmapip1  39937  hgmapvvlem1  39944  hgmapvvlem2  39945  isdomn4  40179  prjspersym  40453  prjspreln0  40455  prjspvs  40456  dffltz  40478  aomclem2  40887  mpaaeu  40982  deg1mhm  41039  gneispace  41751  radcnvrat  41939  bccm1k  41967  disjf1o  42736  supminfxr2  43016  icoiccdif  43069  climrec  43151  climdivf  43160  lptre2pt  43188  0ellimcdiv  43197  limclner  43199  reclimc  43201  cnrefiisplem  43377  cncficcgt0  43436  fperdvper  43467  dvdivcncf  43475  dvnmul  43491  stoweidlem57  43605  dirkercncflem1  43651  fourierdlem24  43679  fourierdlem62  43716  fourierdlem66  43720  elaa2  43782  etransclem35  43817  etransclem47  43829  meadjiunlem  44010  ovnhoilem1  44146  hspmbllem1  44171  fmtnoprmfac1lem  45027  lindssnlvec  45838  logcxp0  45892