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

Syntax hints:   → wi 4   ∈ wcel 2119   ≠ wne 2934   ∖ cdif 3880  {csn 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-v 3433  df-dif 3886  df-sn 4557

This theorem is referenced by:  eldifsnneq  4725  neldifsn  4726  suppssov1  8138  suppssov2  8139  suppss2  8141  suppssfv  8143  sniffsupp  9304  elfi2  9318  fifo  9336  en2other2  9923  finacn  9964  acndom2  9968  dfacacn  10056  kmlem11  10075  acncc  10354  axdc2lem  10362  1div0OLD  11802  elfzodif0  13717  expne0i  14048  incexc  15794  fprodn0f  15948  oddprm  16773  firest  17387  pfxchn  18568  chnind  18579  chnccat  18584  chnrev  18585  symgextf1lem  19387  pmtrmvd  19423  efgsp1  19704  efgredlem  19714  gsummpt1n0  19932  dprdfid  19986  dprdres  19997  dprd2da  20011  dmdprdsplit2lem  20014  ablfac1b  20039  ringelnzr  20496  isdomn4  20689  fidomndrnglem  20745  imadrhmcl  20770  sdrgacs  20774  cntzsdrg  20775  lvecinv  21107  lspsncmp  21110  lspsneq  21116  lspsneu  21117  lspdisjb  21120  lspexch  21123  lvecindp2  21133  cnflddiv  21378  uvcff  21767  frlmssuvc2  21771  frlmup2  21775  lindfrn  21797  f1lindf  21798  psrridm  21938  mplsubrg  21980  mplmon  22012  mplmonmul  22013  coe1tmmul  22264  dmatmul  22481  1marepvsma1  22567  mdetrsca2  22588  mdetrlin2  22591  mdetunilem5  22600  mdetunilem9  22604  maducoeval2  22624  gsummatr01lem3  22641  gsummatr01lem4  22642  gsummatr01  22643  cmpfi  23392  ptpjpre2  23564  alexsublem  24028  ptcmplem2  24037  divcn  24854  divcncf  25433  i1fmullem  25680  itg1addlem4  25685  itg1addlem5  25686  i1fmulc  25689  itg1mulc  25690  i1fres  25691  itg10a  25696  itg1climres  25700  mbfi1fseqlem4  25704  ellimc2  25863  dvcnp2  25906  dvaddbr  25924  dvmulbr  25925  dvcobr  25932  dvcjbr  25935  dvrec  25941  dvrecg  25959  dvcnvlem  25962  dvexp3  25964  dveflem  25965  ftc1lem6  26027  deg1n0ima  26073  ig1peu  26159  plyeq0lem  26194  dgrlem  26213  dgrlb  26220  coemulhi  26238  fta1  26293  aannenlem2  26314  tayl0  26346  taylthlem2  26358  abelthlem7  26422  dcubic  26829  rlimcnp  26948  efrlim  26952  muinv  27175  logexprlim  27207  lgslem1  27279  lgsqr  27333  lgseisenlem2  27358  lgseisenlem4  27360  lgseisen  27361  lgsquadlem1  27362  lgsquad2  27368  m1lgs  27370  dchrisum0re  27495  dchrisum0lema  27496  dchrisum0lem2  27500  dchrisum0lem3  27501  nnne0s  28348  uhgrn0  29155  upgrn0  29177  upgrex  29180  numedglnl  29232  upgrreslem  29392  isuvtx  29483  cusgrexilem2  29530  cusgrexi  29531  structtocusgr  29534  cusgrfilem2  29544  frgrhash2wsp  30421  1div0apr  30557  fmptunsnop  32793  disjdsct  32796  fxpsdrg  33257  elrgspnlem2  33325  elrgspnlem3  33326  domnprodn0  33357  isdrng4  33380  fracfld  33393  lindssn  33462  drngidl  33517  pidufd  33635  1arithufdlem3  33638  dfufd2  33642  zringidom  33643  zringfrac  33646  deg1prod  33675  ig1pmindeg  33694  psrmonmul  33743  assafld  33830  irngnzply1  33884  irngnminplynz  33905  constrsdrg  33968  signstfvneq0  34765  lfuhgr2  35356  cusgredgex  35359  loop1cycl  35374  subfacp1lem1  35416  circum  35911  neibastop1  36596  bj-xpnzexb  37323  bj-restn0b  37458  curf  37974  poimirlem2  37998  poimirlem24  38020  poimirlem25  38021  dvtan  38046  ftc1cnnc  38068  ftc1anclem3  38071  rrndstprj2  38207  lsat0cv  39534  lkreqN  39671  lkrlspeqN  39672  dochnel  41894  djhcvat42  41916  dochsnkr  41973  dochsnkr2cl  41975  lcfl6lem  41999  lcfl8b  42005  lcfrlem16  42059  lcfrlem25  42068  lcfrlem27  42070  lcfrlem33  42076  lcfrlem37  42080  mapdn0  42170  mapdpglem24  42205  mapdindp1  42221  mapdhval2  42227  hdmap1val2  42301  hdmapnzcl  42346  hdmap14lem1  42369  hdmap14lem4a  42372  hdmap14lem6  42374  hgmaprnlem1N  42397  hdmapip1  42417  hgmapvvlem1  42424  hgmapvvlem2  42425  aks6d1c5lem2  42632  resuppsinopn  42849  readvcot  42850  domnexpgn0cl  43018  prjspersym  43066  prjspreln0  43068  prjspvs  43069  dffltz  43093  aomclem2  43509  mpaaeu  43604  deg1mhm  43654  gneispace  44587  radcnvrat  44767  bccm1k  44795  disjf1o  45646  supminfxr2  45920  icoiccdif  45977  climrec  46056  climdivf  46065  lptre2pt  46091  0ellimcdiv  46100  limclner  46102  reclimc  46104  cnrefiisplem  46280  cncficcgt0  46339  fperdvper  46370  dvdivcncf  46378  dvnmul  46394  stoweidlem57  46508  dirkercncflem1  46554  fourierdlem24  46582  fourierdlem62  46619  fourierdlem66  46623  elaa2  46685  etransclem35  46720  etransclem47  46732  meadjiunlem  46916  ovnhoilem1  47052  hspmbllem1  47077  fmtnoprmfac1lem  48050  isubgruhgr  48367  isubgr0uhgr  48372  lindssnlvec  48985  logcxp0  49034