Theorem eldifsni 4744

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

Syntax hints:   → wi 4   ∈ wcel 2113   ≠ wne 2930   ∖ cdif 3896  {csn 4578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-v 3440  df-dif 3902  df-sn 4579

This theorem is referenced by:  eldifsnneq  4745  neldifsn  4746  suppssov1  8137  suppssov2  8138  suppss2  8140  suppssfv  8142  sniffsupp  9301  elfi2  9315  fifo  9333  en2other2  9917  finacn  9958  acndom2  9962  dfacacn  10050  kmlem11  10069  acncc  10348  axdc2lem  10356  1div0OLD  11795  elfzodif0  13684  expne0i  14015  incexc  15758  fprodn0f  15912  oddprm  16736  firest  17350  pfxchn  18531  chnind  18542  chnccat  18547  chnrev  18548  symgextf1lem  19347  pmtrmvd  19383  efgsp1  19664  efgredlem  19674  gsummpt1n0  19892  dprdfid  19946  dprdres  19957  dprd2da  19971  dmdprdsplit2lem  19974  ablfac1b  19999  ringelnzr  20454  isdomn4  20647  fidomndrnglem  20703  imadrhmcl  20728  sdrgacs  20732  cntzsdrg  20733  lvecinv  21066  lspsncmp  21069  lspsneq  21075  lspsneu  21076  lspdisjb  21079  lspexch  21082  lvecindp2  21092  cnflddiv  21353  uvcff  21744  frlmssuvc2  21748  frlmup2  21752  lindfrn  21774  f1lindf  21775  psrridm  21916  mplsubrg  21958  mplmon  21988  mplmonmul  21989  coe1tmmul  22217  dmatmul  22439  1marepvsma1  22525  mdetrsca2  22546  mdetrlin2  22549  mdetunilem5  22558  mdetunilem9  22562  maducoeval2  22582  gsummatr01lem3  22599  gsummatr01lem4  22600  gsummatr01  22601  cmpfi  23350  ptpjpre2  23522  alexsublem  23986  ptcmplem2  23995  divcn  24813  divcncf  25402  i1fmullem  25649  itg1addlem4  25654  itg1addlem5  25655  i1fmulc  25658  itg1mulc  25659  i1fres  25660  itg10a  25665  itg1climres  25669  mbfi1fseqlem4  25673  ellimc2  25832  dvcnp2  25875  dvcnp2OLD  25876  dvaddbr  25894  dvmulbr  25895  dvmulbrOLD  25896  dvcobr  25903  dvcobrOLD  25904  dvcjbr  25907  dvrec  25913  dvrecg  25931  dvcnvlem  25934  dvexp3  25936  dveflem  25937  ftc1lem6  26002  deg1n0ima  26048  ig1peu  26134  plyeq0lem  26169  dgrlem  26188  dgrlb  26195  coemulhi  26213  fta1  26270  aannenlem2  26291  tayl0  26323  taylthlem2  26336  taylthlem2OLD  26337  abelthlem7  26402  dcubic  26810  rlimcnp  26929  efrlim  26933  efrlimOLD  26934  muinv  27157  logexprlim  27190  lgslem1  27262  lgsqr  27316  lgseisenlem2  27341  lgseisenlem4  27343  lgseisen  27344  lgsquadlem1  27345  lgsquad2  27351  m1lgs  27353  dchrisum0re  27478  dchrisum0lema  27479  dchrisum0lem2  27483  dchrisum0lem3  27484  nnne0s  28297  uhgrn0  29089  upgrn0  29111  upgrex  29114  numedglnl  29166  upgrreslem  29326  isuvtx  29417  cusgrexilem2  29464  cusgrexi  29465  structtocusgr  29468  cusgrfilem2  29479  frgrhash2wsp  30356  1div0apr  30492  fmptunsnop  32728  disjdsct  32731  fxpsdrg  33206  elrgspnlem2  33274  elrgspnlem3  33275  domnprodn0  33306  isdrng4  33326  fracfld  33339  lindssn  33408  drngidl  33463  pidufd  33573  1arithufdlem3  33576  dfufd2  33580  zringidom  33581  zringfrac  33584  deg1prod  33613  ig1pmindeg  33632  assafld  33743  irngnzply1  33797  irngnminplynz  33818  constrsdrg  33881  signstfvneq0  34678  lfuhgr2  35262  cusgredgex  35265  loop1cycl  35280  subfacp1lem1  35322  circum  35817  neibastop1  36502  bj-xpnzexb  37105  bj-restn0b  37235  curf  37738  poimirlem2  37762  poimirlem24  37784  poimirlem25  37785  dvtan  37810  ftc1cnnc  37832  ftc1anclem3  37835  rrndstprj2  37971  lsat0cv  39232  lkreqN  39369  lkrlspeqN  39370  dochnel  41592  djhcvat42  41614  dochsnkr  41671  dochsnkr2cl  41673  lcfl6lem  41697  lcfl8b  41703  lcfrlem16  41757  lcfrlem25  41766  lcfrlem27  41768  lcfrlem33  41774  lcfrlem37  41778  mapdn0  41868  mapdpglem24  41903  mapdindp1  41919  mapdhval2  41925  hdmap1val2  41999  hdmapnzcl  42044  hdmap14lem1  42067  hdmap14lem4a  42070  hdmap14lem6  42072  hgmaprnlem1N  42095  hdmapip1  42115  hgmapvvlem1  42122  hgmapvvlem2  42123  aks6d1c5lem2  42331  resuppsinopn  42560  readvcot  42561  domnexpgn0cl  42720  prjspersym  42792  prjspreln0  42794  prjspvs  42795  dffltz  42819  aomclem2  43239  mpaaeu  43334  deg1mhm  43384  gneispace  44317  radcnvrat  44497  bccm1k  44525  disjf1o  45377  supminfxr2  45655  icoiccdif  45712  climrec  45791  climdivf  45800  lptre2pt  45826  0ellimcdiv  45835  limclner  45837  reclimc  45839  cnrefiisplem  46015  cncficcgt0  46074  fperdvper  46105  dvdivcncf  46113  dvnmul  46129  stoweidlem57  46243  dirkercncflem1  46289  fourierdlem24  46317  fourierdlem62  46354  fourierdlem66  46358  elaa2  46420  etransclem35  46455  etransclem47  46467  meadjiunlem  46651  ovnhoilem1  46787  hspmbllem1  46812  fmtnoprmfac1lem  47752  isubgruhgr  48056  isubgr0uhgr  48061  lindssnlvec  48674  logcxp0  48723