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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ≠ wne 2955   ∖ cdif 4045  {csn 4583

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-dif 4047  df-sn 4584

This theorem is used by:  eldifsnneq  4753  neldifsn  4754  suppssov1  8214  suppssov2  8215  suppss2  8217  suppssfv  8219  curf  8890  sniffsupp  9392  elfi2  9406  fifo  9424  en2other2  10088  finacn  10129  acndom2  10133  dfacacn  10220  kmlem11  10239  acncc  10518  axdc2lem  10526  elfzodif0  13905  expne0i  14237  incexc  16006  fprodn0f  16158  oddprm  16988  firest  17603  pfxchn  18784  chnind  18795  chnccat  18800  chnrev  18801  symgextf1lem  19634  pmtrmvd  19670  efgsp1  19951  efgredlem  19961  gsummpt1n0  20179  dprdfid  20233  dprdres  20244  dprd2da  20258  dmdprdsplit2lem  20261  ablfac1b  20286  ringelnzr  20774  isdomn4  20967  isdrng4  20992  fidomndrnglem  21030  imadrhmcl  21054  sdrgacs  21058  cntzsdrg  21059  lvecinv  21391  lspsncmp  21394  lspsneq  21400  lspsneu  21401  lspdisjb  21404  lspexch  21407  lvecindp2  21417  drngidl  21539  cnflddiv  21708  uvcff  22097  frlmssuvc2  22101  frlmup2  22105  lindfrn  22127  f1lindf  22128  psrridm  22270  mplsubrg  22312  mplmon  22344  mplmonmul  22345  coe1tmmul  22596  dmatmul  22812  1marepvsma1  22898  mdetrsca2  22919  mdetrlin2  22922  mdetunilem5  22931  mdetunilem9  22935  maducoeval2  22955  gsummatr01lem3  22972  gsummatr01lem4  22973  gsummatr01  22974  cmpfi  23726  ptpjpre2  23899  alexsublem  24363  ptcmplem2  24372  divcn  25189  divcncf  25768  i1fmullem  26015  itg1addlem4  26020  itg1addlem5  26021  i1fmulc  26024  itg1mulc  26025  i1fres  26026  itg10a  26031  itg1climres  26035  mbfi1fseqlem4  26039  ellimc2  26197  dvcnp2  26240  dvaddbr  26258  dvmulbr  26259  dvcobr  26266  dvcjbr  26269  dvrec  26275  dvrecg  26293  dvcnvlem  26296  dvexp3  26298  dveflem  26299  ftc1lem6  26361  deg1n0ima  26407  ig1peu  26493  plyeq0lem  26529  dgrlem  26548  dgrlb  26555  coemulhi  26573  fta1  26629  preimaaa  26646  aannenlem2  26656  tayl0  26689  taylthlem2  26701  abelthlem7  26765  dcubic  27174  rlimcnp  27293  efrlim  27297  muinv  27520  logexprlim  27552  lgslem1  27624  lgsqr  27678  lgseisenlem2  27703  lgseisenlem4  27705  lgseisen  27706  lgsquad2  27713  m1lgs  27715  dchrisum0re  27840  dchrisum0lema  27841  dchrisum0lem2  27845  dchrisum0lem3  27846  nnne0s  28723  uhgrn0  29645  upgrn0  29667  upgrex  29670  numedglnl  29722  lfuhgr2  29727  upgrreslem  29885  isuvtx  29976  cusgrexilem2  30023  cusgrexi  30024  structtocusgr  30027  cusgrfilem2  30037  loop1cycl  30744  frgrhash2wsp  30933  1div0apr  31069  fmptunsnop  33293  disjdsct  33296  fxpsdrg  33736  elrgspnlem2  33804  elrgspnlem3  33805  domnprodn0  33839  fracfld  33870  lindssn  33933  pidufd  34075  1arithufdlem3  34078  dfufd2  34082  zringidom  34083  zringfrac  34086  deg1prod  34115  ig1pmindeg  34134  psrmonmul  34182  assafld  34269  irngnzply1  34323  irngnminplynz  34344  constrsdrg  34407  signstfvneq0  35201  cusgredgex  35906  subfacp1lem1  35944  circum  36439  neibastop1  37147  bj-xpnzexb  37874  bj-restn0b  38012  poimirlem2  38541  poimirlem24  38563  poimirlem25  38564  dvtan  38589  ftc1cnnc  38611  ftc1anclem3  38614  rrndstprj2  38766  lsat0cv  40091  lkreqN  40228  lkrlspeqN  40229  dochnel  42451  djhcvat42  42473  dochsnkr  42530  dochsnkr2cl  42532  lcfl6lem  42556  lcfl8b  42562  lcfrlem16  42616  lcfrlem25  42625  lcfrlem27  42627  lcfrlem33  42633  lcfrlem37  42637  mapdn0  42727  mapdpglem24  42762  mapdindp1  42778  mapdhval2  42784  hdmap1val2  42858  hdmapnzcl  42903  hdmap14lem1  42926  hdmap14lem4a  42929  hdmap14lem6  42931  hgmaprnlem1N  42954  hdmapip1  42974  hgmapvvlem1  42981  hgmapvvlem2  42982  aks6d1c5lem2  43189  resuppsinopn  43415  readvcot  43416  domnexpgn0cl  43585  prjspersym  43636  prjspreln0  43638  prjspvs  43639  dffltz  43671  aomclem2  44057  mpaaeu  44152  deg1mhm  44202  gneispace  45134  radcnvrat  45298  bccm1k  45326  disjf1o  46206  supminfxr2  46479  icoiccdif  46536  climrec  46615  climdivf  46624  lptre2pt  46650  0ellimcdiv  46659  limclner  46661  reclimc  46663  cnrefiisplem  46839  cncficcgt0  46898  fperdvper  46929  dvdivcncf  46937  dvnmul  46953  stoweidlem57  47067  dirkercncflem1  47113  fourierdlem24  47141  fourierdlem62  47178  fourierdlem66  47182  elaa2  47244  etransclem35  47279  etransclem47  47291  meadjiunlem  47475  ovnhoilem1  47611  hspmbllem1  47636  fmtnoprmfac1lem  48649  isubgruhgr  48966  isubgr0uhgr  48971  lindssnlvec  49598  logcxp0  49647