Theorem eldifsni 4790

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2940   ∖ cdif 3948  {csn 4626

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-sn 4627

This theorem is referenced by:  eldifsnneq  4791  neldifsn  4792  suppssov1  8222  suppssov2  8223  suppss2  8225  suppssfv  8227  sniffsupp  9440  elfi2  9454  fifo  9472  en2other2  10049  finacn  10090  acndom2  10094  dfacacn  10182  kmlem11  10201  acncc  10480  axdc2lem  10488  1div0OLD  11923  expne0i  14135  incexc  15873  fprodn0f  16027  oddprm  16848  firest  17477  symgextf1lem  19438  pmtrmvd  19474  efgsp1  19755  efgredlem  19765  gsummpt1n0  19983  dprdfid  20037  dprdres  20048  dprd2da  20062  dmdprdsplit2lem  20065  ablfac1b  20090  ringelnzr  20523  isdomn4  20716  fidomndrnglem  20773  imadrhmcl  20798  sdrgacs  20802  cntzsdrg  20803  lvecinv  21115  lspsncmp  21118  lspsneq  21124  lspsneu  21125  lspdisjb  21128  lspexch  21131  lvecindp2  21141  cnflddiv  21413  uvcff  21811  frlmssuvc2  21815  frlmup2  21819  lindfrn  21841  f1lindf  21842  psrridm  21983  mplsubrg  22025  mplmon  22053  mplmonmul  22054  coe1tmmul  22280  dmatmul  22503  1marepvsma1  22589  mdetrsca2  22610  mdetrlin2  22613  mdetunilem5  22622  mdetunilem9  22626  maducoeval2  22646  gsummatr01lem3  22663  gsummatr01lem4  22664  gsummatr01  22665  cmpfi  23416  ptpjpre2  23588  alexsublem  24052  ptcmplem2  24061  divcn  24892  divcncf  25482  i1fmullem  25729  itg1addlem4  25734  itg1addlem5  25735  i1fmulc  25738  itg1mulc  25739  i1fres  25740  itg10a  25745  itg1climres  25749  mbfi1fseqlem4  25753  ellimc2  25912  dvcnp2  25955  dvcnp2OLD  25956  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvcobr  25983  dvcobrOLD  25984  dvcjbr  25987  dvrec  25993  dvrecg  26011  dvcnvlem  26014  dvexp3  26016  dveflem  26017  ftc1lem6  26082  deg1n0ima  26128  ig1peu  26214  plyeq0lem  26249  dgrlem  26268  dgrlb  26275  coemulhi  26293  fta1  26350  aannenlem2  26371  tayl0  26403  taylthlem2  26416  taylthlem2OLD  26417  abelthlem7  26482  dcubic  26889  rlimcnp  27008  efrlim  27012  efrlimOLD  27013  muinv  27236  logexprlim  27269  lgslem1  27341  lgsqr  27395  lgseisenlem2  27420  lgseisenlem4  27422  lgseisen  27423  lgsquadlem1  27424  lgsquad2  27430  m1lgs  27432  dchrisum0re  27557  dchrisum0lema  27558  dchrisum0lem2  27562  dchrisum0lem3  27563  nnne0s  28340  uhgrn0  29084  upgrn0  29106  upgrex  29109  numedglnl  29161  upgrreslem  29321  isuvtx  29412  cusgrexilem2  29459  cusgrexi  29460  structtocusgr  29463  cusgrfilem2  29474  frgrhash2wsp  30351  1div0apr  30487  fmptunsnop  32709  disjdsct  32712  elfzodif0  32796  pfxchn  32999  chnind  33001  elrgspnlem2  33247  elrgspnlem3  33248  domnprodn0  33279  isdrng4  33298  fracfld  33310  lindssn  33406  drngidl  33461  pidufd  33571  1arithufdlem3  33574  dfufd2  33578  zringidom  33579  zringfrac  33582  ig1pmindeg  33622  assafld  33688  irngnzply1  33741  irngnminplynz  33755  signstfvneq0  34587  lfuhgr2  35124  cusgredgex  35127  loop1cycl  35142  subfacp1lem1  35184  circum  35679  neibastop1  36360  bj-xpnzexb  36962  bj-restn0b  37092  curf  37605  poimirlem2  37629  poimirlem24  37651  poimirlem25  37652  dvtan  37677  ftc1cnnc  37699  ftc1anclem3  37702  rrndstprj2  37838  lsat0cv  39034  lkreqN  39171  lkrlspeqN  39172  dochnel  41395  djhcvat42  41417  dochsnkr  41474  dochsnkr2cl  41476  lcfl6lem  41500  lcfl8b  41506  lcfrlem16  41560  lcfrlem25  41569  lcfrlem27  41571  lcfrlem33  41577  lcfrlem37  41581  mapdn0  41671  mapdpglem24  41706  mapdindp1  41722  mapdhval2  41728  hdmap1val2  41802  hdmapnzcl  41847  hdmap14lem1  41870  hdmap14lem4a  41873  hdmap14lem6  41875  hgmaprnlem1N  41898  hdmapip1  41918  hgmapvvlem1  41925  hgmapvvlem2  41926  aks6d1c5lem2  42139  resuppsinopn  42393  readvcot  42394  domnexpgn0cl  42533  prjspersym  42617  prjspreln0  42619  prjspvs  42620  dffltz  42644  aomclem2  43067  mpaaeu  43162  deg1mhm  43212  gneispace  44147  radcnvrat  44333  bccm1k  44361  disjf1o  45196  supminfxr2  45480  icoiccdif  45537  climrec  45618  climdivf  45627  lptre2pt  45655  0ellimcdiv  45664  limclner  45666  reclimc  45668  cnrefiisplem  45844  cncficcgt0  45903  fperdvper  45934  dvdivcncf  45942  dvnmul  45958  stoweidlem57  46072  dirkercncflem1  46118  fourierdlem24  46146  fourierdlem62  46183  fourierdlem66  46187  elaa2  46249  etransclem35  46284  etransclem47  46296  meadjiunlem  46480  ovnhoilem1  46616  hspmbllem1  46641  fmtnoprmfac1lem  47551  isubgruhgr  47854  isubgr0uhgr  47859  lindssnlvec  48403  logcxp0  48456