Theorem eldifsni 4726

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

Syntax hints:   → wi 4   ∈ wcel 2121   ≠ wne 2936   ∖ cdif 3882  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-v 3435  df-dif 3888  df-sn 4559

This theorem is referenced by:  eldifsnneq  4727  neldifsn  4728  suppssov1  8141  suppssov2  8142  suppss2  8144  suppssfv  8146  sniffsupp  9307  elfi2  9321  fifo  9339  en2other2  9926  finacn  9967  acndom2  9971  dfacacn  10059  kmlem11  10078  acncc  10357  axdc2lem  10365  1div0OLD  11805  elfzodif0  13720  expne0i  14051  incexc  15797  fprodn0f  15951  oddprm  16776  firest  17390  pfxchn  18571  chnind  18582  chnccat  18587  chnrev  18588  symgextf1lem  19390  pmtrmvd  19426  efgsp1  19707  efgredlem  19717  gsummpt1n0  19935  dprdfid  19989  dprdres  20000  dprd2da  20014  dmdprdsplit2lem  20017  ablfac1b  20042  ringelnzr  20499  isdomn4  20692  fidomndrnglem  20748  imadrhmcl  20773  sdrgacs  20777  cntzsdrg  20778  lvecinv  21110  lspsncmp  21113  lspsneq  21119  lspsneu  21120  lspdisjb  21123  lspexch  21126  lvecindp2  21136  cnflddiv  21381  uvcff  21770  frlmssuvc2  21774  frlmup2  21778  lindfrn  21800  f1lindf  21801  psrridm  21941  mplsubrg  21983  mplmon  22015  mplmonmul  22016  coe1tmmul  22267  dmatmul  22484  1marepvsma1  22570  mdetrsca2  22591  mdetrlin2  22594  mdetunilem5  22603  mdetunilem9  22607  maducoeval2  22627  gsummatr01lem3  22644  gsummatr01lem4  22645  gsummatr01  22646  cmpfi  23395  ptpjpre2  23567  alexsublem  24031  ptcmplem2  24040  divcn  24857  divcncf  25436  i1fmullem  25683  itg1addlem4  25688  itg1addlem5  25689  i1fmulc  25692  itg1mulc  25693  i1fres  25694  itg10a  25699  itg1climres  25703  mbfi1fseqlem4  25707  ellimc2  25866  dvcnp2  25909  dvaddbr  25927  dvmulbr  25928  dvcobr  25935  dvcjbr  25938  dvrec  25944  dvrecg  25962  dvcnvlem  25965  dvexp3  25967  dveflem  25968  ftc1lem6  26030  deg1n0ima  26076  ig1peu  26162  plyeq0lem  26197  dgrlem  26216  dgrlb  26223  coemulhi  26241  fta1  26296  aannenlem2  26317  tayl0  26349  taylthlem2  26361  abelthlem7  26425  dcubic  26832  rlimcnp  26951  efrlim  26955  muinv  27178  logexprlim  27210  lgslem1  27282  lgsqr  27336  lgseisenlem2  27361  lgseisenlem4  27363  lgseisen  27364  lgsquadlem1  27365  lgsquad2  27371  m1lgs  27373  dchrisum0re  27498  dchrisum0lema  27499  dchrisum0lem2  27503  dchrisum0lem3  27504  nnne0s  28351  uhgrn0  29158  upgrn0  29180  upgrex  29183  numedglnl  29235  upgrreslem  29395  isuvtx  29486  cusgrexilem2  29533  cusgrexi  29534  structtocusgr  29537  cusgrfilem2  29547  frgrhash2wsp  30424  1div0apr  30560  fmptunsnop  32796  disjdsct  32799  fxpsdrg  33260  elrgspnlem2  33328  elrgspnlem3  33329  domnprodn0  33360  isdrng4  33383  fracfld  33396  lindssn  33465  drngidl  33520  pidufd  33638  1arithufdlem3  33641  dfufd2  33645  zringidom  33646  zringfrac  33649  deg1prod  33678  ig1pmindeg  33697  psrmonmul  33746  assafld  33833  irngnzply1  33887  irngnminplynz  33908  constrsdrg  33971  signstfvneq0  34768  lfuhgr2  35362  cusgredgex  35365  loop1cycl  35380  subfacp1lem1  35422  circum  35917  neibastop1  36602  bj-xpnzexb  37329  bj-restn0b  37464  curf  37980  poimirlem2  38004  poimirlem24  38026  poimirlem25  38027  dvtan  38052  ftc1cnnc  38074  ftc1anclem3  38077  rrndstprj2  38213  lsat0cv  39540  lkreqN  39677  lkrlspeqN  39678  dochnel  41900  djhcvat42  41922  dochsnkr  41979  dochsnkr2cl  41981  lcfl6lem  42005  lcfl8b  42011  lcfrlem16  42065  lcfrlem25  42074  lcfrlem27  42076  lcfrlem33  42082  lcfrlem37  42086  mapdn0  42176  mapdpglem24  42211  mapdindp1  42227  mapdhval2  42233  hdmap1val2  42307  hdmapnzcl  42352  hdmap14lem1  42375  hdmap14lem4a  42378  hdmap14lem6  42380  hgmaprnlem1N  42403  hdmapip1  42423  hgmapvvlem1  42430  hgmapvvlem2  42431  aks6d1c5lem2  42638  resuppsinopn  42855  readvcot  42856  domnexpgn0cl  43024  prjspersym  43072  prjspreln0  43074  prjspvs  43075  dffltz  43099  aomclem2  43515  mpaaeu  43610  deg1mhm  43660  gneispace  44593  radcnvrat  44773  bccm1k  44801  disjf1o  45652  supminfxr2  45926  icoiccdif  45983  climrec  46062  climdivf  46071  lptre2pt  46097  0ellimcdiv  46106  limclner  46108  reclimc  46110  cnrefiisplem  46286  cncficcgt0  46345  fperdvper  46376  dvdivcncf  46384  dvnmul  46400  stoweidlem57  46514  dirkercncflem1  46560  fourierdlem24  46588  fourierdlem62  46625  fourierdlem66  46629  elaa2  46691  etransclem35  46726  etransclem47  46738  meadjiunlem  46922  ovnhoilem1  47058  hspmbllem1  47083  fmtnoprmfac1lem  48056  isubgruhgr  48373  isubgr0uhgr  48378  lindssnlvec  48991  logcxp0  49040