Theorem eldifsni 4753

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 503	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) → 𝐴 ≠ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2955   ∖ cdif 3896  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-dif 3902  df-sn 4585

This theorem is used by:  eldifsnneq  4754  neldifsn  4755  suppssov1  8193  suppssov2  8194  suppss2  8196  suppssfv  8198  curf  8869  sniffsupp  9370  elfi2  9384  fifo  9402  en2other2  10045  finacn  10086  acndom2  10090  dfacacn  10177  kmlem11  10196  acncc  10475  axdc2lem  10483  elfzodif0  13859  expne0i  14191  incexc  15959  fprodn0f  16111  oddprm  16935  firest  17550  pfxchn  18731  chnind  18742  chnccat  18747  chnrev  18748  symgextf1lem  19581  pmtrmvd  19617  efgsp1  19898  efgredlem  19908  gsummpt1n0  20126  dprdfid  20180  dprdres  20191  dprd2da  20205  dmdprdsplit2lem  20208  ablfac1b  20233  ringelnzr  20721  isdomn4  20914  isdrng4  20939  fidomndrnglem  20977  imadrhmcl  21001  sdrgacs  21005  cntzsdrg  21006  lvecinv  21338  lspsncmp  21341  lspsneq  21347  lspsneu  21348  lspdisjb  21351  lspexch  21354  lvecindp2  21364  drngidl  21486  cnflddiv  21655  uvcff  22044  frlmssuvc2  22048  frlmup2  22052  lindfrn  22074  f1lindf  22075  psrridm  22217  mplsubrg  22259  mplmon  22291  mplmonmul  22292  coe1tmmul  22543  dmatmul  22759  1marepvsma1  22845  mdetrsca2  22866  mdetrlin2  22869  mdetunilem5  22878  mdetunilem9  22882  maducoeval2  22902  gsummatr01lem3  22919  gsummatr01lem4  22920  gsummatr01  22921  cmpfi  23673  ptpjpre2  23846  alexsublem  24310  ptcmplem2  24319  divcn  25136  divcncf  25715  i1fmullem  25962  itg1addlem4  25967  itg1addlem5  25968  i1fmulc  25971  itg1mulc  25972  i1fres  25973  itg10a  25978  itg1climres  25982  mbfi1fseqlem4  25986  ellimc2  26144  dvcnp2  26187  dvaddbr  26205  dvmulbr  26206  dvcobr  26213  dvcjbr  26216  dvrec  26222  dvrecg  26240  dvcnvlem  26243  dvexp3  26245  dveflem  26246  ftc1lem6  26308  deg1n0ima  26354  ig1peu  26440  plyeq0lem  26476  dgrlem  26495  dgrlb  26502  coemulhi  26520  fta1  26578  preimaaa  26595  aannenlem2  26605  tayl0  26638  taylthlem2  26650  abelthlem7  26714  dcubic  27123  rlimcnp  27242  efrlim  27246  muinv  27469  logexprlim  27501  lgslem1  27573  lgsqr  27627  lgseisenlem2  27652  lgseisenlem4  27654  lgseisen  27655  lgsquadlem1  27656  lgsquad2  27662  m1lgs  27664  dchrisum0re  27789  dchrisum0lema  27790  dchrisum0lem2  27794  dchrisum0lem3  27795  nnne0s  28642  uhgrn0  29564  upgrn0  29586  upgrex  29589  numedglnl  29641  lfuhgr2  29646  upgrreslem  29804  isuvtx  29895  cusgrexilem2  29942  cusgrexi  29943  structtocusgr  29946  cusgrfilem2  29956  loop1cycl  30663  frgrhash2wsp  30852  1div0apr  30988  fmptunsnop  33212  disjdsct  33215  fxpsdrg  33655  elrgspnlem2  33723  elrgspnlem3  33724  domnprodn0  33758  fracfld  33789  lindssn  33852  pidufd  33994  1arithufdlem3  33997  dfufd2  34001  zringidom  34002  zringfrac  34005  deg1prod  34034  ig1pmindeg  34053  psrmonmul  34101  assafld  34188  irngnzply1  34242  irngnminplynz  34263  constrsdrg  34326  signstfvneq0  35121  cusgredgex  35821  subfacp1lem1  35859  circum  36354  neibastop1  37063  bj-xpnzexb  37790  bj-restn0b  37926  poimirlem2  38454  poimirlem24  38476  poimirlem25  38477  dvtan  38502  ftc1cnnc  38524  ftc1anclem3  38527  rrndstprj2  38679  lsat0cv  40004  lkreqN  40141  lkrlspeqN  40142  dochnel  42364  djhcvat42  42386  dochsnkr  42443  dochsnkr2cl  42445  lcfl6lem  42469  lcfl8b  42475  lcfrlem16  42529  lcfrlem25  42538  lcfrlem27  42540  lcfrlem33  42546  lcfrlem37  42550  mapdn0  42640  mapdpglem24  42675  mapdindp1  42691  mapdhval2  42697  hdmap1val2  42771  hdmapnzcl  42816  hdmap14lem1  42839  hdmap14lem4a  42842  hdmap14lem6  42844  hgmaprnlem1N  42867  hdmapip1  42887  hgmapvvlem1  42894  hgmapvvlem2  42895  aks6d1c5lem2  43102  resuppsinopn  43336  readvcot  43337  domnexpgn0cl  43503  prjspersym  43551  prjspreln0  43553  prjspvs  43554  dffltz  43578  aomclem2  43994  mpaaeu  44089  deg1mhm  44139  gneispace  45072  radcnvrat  45236  bccm1k  45264  disjf1o  46121  supminfxr2  46395  icoiccdif  46452  climrec  46531  climdivf  46540  lptre2pt  46566  0ellimcdiv  46575  limclner  46577  reclimc  46579  cnrefiisplem  46755  cncficcgt0  46814  fperdvper  46845  dvdivcncf  46853  dvnmul  46869  stoweidlem57  46983  dirkercncflem1  47029  fourierdlem24  47057  fourierdlem62  47094  fourierdlem66  47098  elaa2  47160  etransclem35  47195  etransclem47  47207  meadjiunlem  47391  ovnhoilem1  47527  hspmbllem1  47552  fmtnoprmfac1lem  48565  isubgruhgr  48882  isubgr0uhgr  48887  lindssnlvec  49514  logcxp0  49563