Theorem eldifsni 4752

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

Syntax hints:   → wi 4   ∈ wcel 2144   ≠ wne 2959   ∖ cdif 3903  {csn 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ne 2960  df-v 3458  df-dif 3909  df-sn 4585

This theorem is referenced by:  eldifsnneq  4753  neldifsn  4754  suppssov1  8179  suppssov2  8180  suppss2  8182  suppssfv  8184  sniffsupp  9348  elfi2  9362  fifo  9380  en2other2  9967  finacn  10008  acndom2  10012  dfacacn  10100  kmlem11  10119  acncc  10399  axdc2lem  10407  elfzodif0  13778  expne0i  14109  incexc  15869  fprodn0f  16023  oddprm  16848  firest  17463  pfxchn  18644  chnind  18655  chnccat  18660  chnrev  18661  symgextf1lem  19462  pmtrmvd  19498  efgsp1  19779  efgredlem  19789  gsummpt1n0  20007  dprdfid  20061  dprdres  20072  dprd2da  20086  dmdprdsplit2lem  20089  ablfac1b  20114  ringelnzr  20575  isdomn4  20768  fidomndrnglem  20824  imadrhmcl  20848  sdrgacs  20852  cntzsdrg  20853  lvecinv  21185  lspsncmp  21188  lspsneq  21194  lspsneu  21195  lspdisjb  21198  lspexch  21201  lvecindp2  21211  cnflddiv  21456  uvcff  21845  frlmssuvc2  21849  frlmup2  21853  lindfrn  21875  f1lindf  21876  psrridm  22016  mplsubrg  22058  mplmon  22090  mplmonmul  22091  coe1tmmul  22342  dmatmul  22559  1marepvsma1  22645  mdetrsca2  22666  mdetrlin2  22669  mdetunilem5  22678  mdetunilem9  22682  maducoeval2  22702  gsummatr01lem3  22719  gsummatr01lem4  22720  gsummatr01  22721  cmpfi  23470  ptpjpre2  23642  alexsublem  24106  ptcmplem2  24115  divcn  24932  divcncf  25511  i1fmullem  25758  itg1addlem4  25763  itg1addlem5  25764  i1fmulc  25767  itg1mulc  25768  i1fres  25769  itg10a  25774  itg1climres  25778  mbfi1fseqlem4  25782  ellimc2  25941  dvcnp2  25984  dvaddbr  26002  dvmulbr  26003  dvcobr  26010  dvcjbr  26013  dvrec  26019  dvrecg  26037  dvcnvlem  26040  dvexp3  26042  dveflem  26043  ftc1lem6  26105  deg1n0ima  26151  ig1peu  26237  plyeq0lem  26272  dgrlem  26291  dgrlb  26298  coemulhi  26316  fta1  26374  aannenlem2  26395  tayl0  26427  taylthlem2  26439  abelthlem7  26503  dcubic  26913  rlimcnp  27032  efrlim  27036  muinv  27259  logexprlim  27291  lgslem1  27363  lgsqr  27417  lgseisenlem2  27442  lgseisenlem4  27444  lgseisen  27445  lgsquadlem1  27446  lgsquad2  27452  m1lgs  27454  dchrisum0re  27579  dchrisum0lema  27580  dchrisum0lem2  27584  dchrisum0lem3  27585  nnne0s  28432  uhgrn0  29270  upgrn0  29292  upgrex  29295  numedglnl  29347  upgrreslem  29507  isuvtx  29598  cusgrexilem2  29645  cusgrexi  29646  structtocusgr  29649  cusgrfilem2  29659  frgrhash2wsp  30536  1div0apr  30672  fmptunsnop  32904  disjdsct  32907  fxpsdrg  33357  elrgspnlem2  33426  elrgspnlem3  33427  domnprodn0  33461  isdrng4  33484  fracfld  33497  lindssn  33566  drngidl  33621  pidufd  33741  1arithufdlem3  33744  dfufd2  33748  zringidom  33749  zringfrac  33752  deg1prod  33781  ig1pmindeg  33800  psrmonmul  33849  assafld  33936  irngnzply1  33990  irngnminplynz  34011  constrsdrg  34074  signstfvneq0  34868  lfuhgr2  35474  cusgredgex  35477  loop1cycl  35492  subfacp1lem1  35534  circum  36029  neibastop1  36724  bj-xpnzexb  37451  bj-restn0b  37586  curf  38102  poimirlem2  38126  poimirlem24  38148  poimirlem25  38149  dvtan  38174  ftc1cnnc  38196  ftc1anclem3  38199  rrndstprj2  38335  lsat0cv  39662  lkreqN  39799  lkrlspeqN  39800  dochnel  42022  djhcvat42  42044  dochsnkr  42101  dochsnkr2cl  42103  lcfl6lem  42127  lcfl8b  42133  lcfrlem16  42187  lcfrlem25  42196  lcfrlem27  42198  lcfrlem33  42204  lcfrlem37  42208  mapdn0  42298  mapdpglem24  42333  mapdindp1  42349  mapdhval2  42355  hdmap1val2  42429  hdmapnzcl  42474  hdmap14lem1  42497  hdmap14lem4a  42500  hdmap14lem6  42502  hgmaprnlem1N  42525  hdmapip1  42545  hgmapvvlem1  42552  hgmapvvlem2  42553  aks6d1c5lem2  42760  resuppsinopn  42977  readvcot  42978  domnexpgn0cl  43146  prjspersym  43194  prjspreln0  43196  prjspvs  43197  dffltz  43221  aomclem2  43637  mpaaeu  43732  deg1mhm  43782  gneispace  44715  radcnvrat  44895  bccm1k  44923  disjf1o  45774  supminfxr2  46048  icoiccdif  46105  climrec  46184  climdivf  46193  lptre2pt  46219  0ellimcdiv  46228  limclner  46230  reclimc  46232  cnrefiisplem  46408  cncficcgt0  46467  fperdvper  46498  dvdivcncf  46506  dvnmul  46522  stoweidlem57  46636  dirkercncflem1  46682  fourierdlem24  46710  fourierdlem62  46747  fourierdlem66  46751  elaa2  46813  etransclem35  46848  etransclem47  46860  meadjiunlem  47044  ovnhoilem1  47180  hspmbllem1  47205  fmtnoprmfac1lem  48178  isubgruhgr  48495  isubgr0uhgr  48500  lindssnlvec  49113  logcxp0  49162