Theorem eldifsni 4794

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

Syntax hints:   → wi 4   ∈ wcel 2107   ≠ wne 2941   ∖ cdif 3946  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3952  df-sn 4630

This theorem is referenced by:  eldifsnneq  4795  neldifsn  4796  suppssov1  8183  suppss2  8185  suppssfv  8187  sniffsupp  9395  elfi2  9409  fifo  9427  en2other2  10004  finacn  10045  acndom2  10049  dfacacn  10136  kmlem11  10155  acncc  10435  axdc2lem  10443  1div0  11873  expne0i  14060  incexc  15783  fprodn0f  15935  oddprm  16743  firest  17378  symgextf1lem  19288  pmtrmvd  19324  efgsp1  19605  efgredlem  19615  gsummpt1n0  19833  dprdfid  19887  dprdres  19898  dprd2da  19912  dmdprdsplit2lem  19915  ablfac1b  19940  ringelnzr  20300  imadrhmcl  20413  sdrgacs  20417  cntzsdrg  20418  lvecinv  20726  lspsncmp  20729  lspsneq  20735  lspsneu  20736  lspdisjb  20739  lspexch  20742  lvecindp2  20752  isdomn4  20918  fidomndrnglem  20925  uvcff  21346  frlmssuvc2  21350  frlmup2  21354  lindfrn  21376  f1lindf  21377  psrridm  21524  mplsubrg  21564  mplmon  21590  mplmonmul  21591  coe1tmmul  21799  dmatmul  21999  1marepvsma1  22085  mdetrsca2  22106  mdetrlin2  22109  mdetunilem5  22118  mdetunilem9  22122  maducoeval2  22142  gsummatr01lem3  22159  gsummatr01lem4  22160  gsummatr01  22161  cmpfi  22912  ptpjpre2  23084  alexsublem  23548  ptcmplem2  23557  divcncf  24964  i1fmullem  25211  itg1addlem4  25216  itg1addlem4OLD  25217  itg1addlem5  25218  i1fmulc  25221  itg1mulc  25222  i1fres  25223  itg10a  25228  itg1climres  25232  mbfi1fseqlem4  25236  ellimc2  25394  dvcnp2  25437  dvaddbr  25455  dvmulbr  25456  dvcobr  25463  dvcjbr  25466  dvrec  25472  dvrecg  25490  dvcnvlem  25493  dvexp3  25495  dveflem  25496  ftc1lem6  25558  deg1n0ima  25607  ig1peu  25689  plyeq0lem  25724  dgrlem  25743  dgrlb  25750  coemulhi  25768  fta1  25821  aannenlem2  25842  tayl0  25874  taylthlem2  25886  abelthlem7  25950  dcubic  26351  rlimcnp  26470  efrlim  26474  muinv  26697  logexprlim  26728  lgslem1  26800  lgsqr  26854  lgseisenlem2  26879  lgseisenlem4  26881  lgseisen  26882  lgsquadlem1  26883  lgsquad2  26889  m1lgs  26891  dchrisum0re  27016  dchrisum0lema  27017  dchrisum0lem2  27021  dchrisum0lem3  27022  uhgrn0  28327  upgrn0  28349  upgrex  28352  numedglnl  28404  upgrreslem  28561  isuvtx  28652  cusgrexilem2  28699  cusgrexi  28700  structtocusgr  28703  cusgrfilem2  28713  frgrhash2wsp  29585  1div0apr  29721  disjdsct  31924  isdrng4  32395  lindssn  32494  drngidl  32551  ig1pmindeg  32671  irngnzply1  32755  irngnminplynz  32771  signstfvneq0  33583  lfuhgr2  34109  cusgredgex  34112  loop1cycl  34128  subfacp1lem1  34170  circum  34659  gg-dvcnp2  35174  gg-dvmulbr  35175  gg-dvcobr  35176  neibastop1  35244  bj-xpnzexb  35842  bj-restn0b  35972  curf  36466  poimirlem2  36490  poimirlem24  36512  poimirlem25  36513  dvtan  36538  ftc1cnnc  36560  ftc1anclem3  36563  rrndstprj2  36699  lsat0cv  37903  lkreqN  38040  lkrlspeqN  38041  dochnel  40264  djhcvat42  40286  dochsnkr  40343  dochsnkr2cl  40345  lcfl6lem  40369  lcfl8b  40375  lcfrlem16  40429  lcfrlem25  40438  lcfrlem27  40440  lcfrlem33  40446  lcfrlem37  40450  mapdn0  40540  mapdpglem24  40575  mapdindp1  40591  mapdhval2  40597  hdmap1val2  40671  hdmapnzcl  40716  hdmap14lem1  40739  hdmap14lem4a  40742  hdmap14lem6  40744  hgmaprnlem1N  40767  hdmapip1  40787  hgmapvvlem1  40794  hgmapvvlem2  40795  prjspersym  41349  prjspreln0  41351  prjspvs  41352  dffltz  41376  aomclem2  41797  mpaaeu  41892  deg1mhm  41949  gneispace  42885  radcnvrat  43073  bccm1k  43101  disjf1o  43889  supminfxr2  44179  icoiccdif  44237  climrec  44319  climdivf  44328  lptre2pt  44356  0ellimcdiv  44365  limclner  44367  reclimc  44369  cnrefiisplem  44545  cncficcgt0  44604  fperdvper  44635  dvdivcncf  44643  dvnmul  44659  stoweidlem57  44773  dirkercncflem1  44819  fourierdlem24  44847  fourierdlem62  44884  fourierdlem66  44888  elaa2  44950  etransclem35  44985  etransclem47  44997  meadjiunlem  45181  ovnhoilem1  45317  hspmbllem1  45342  fmtnoprmfac1lem  46232  lindssnlvec  47167  logcxp0  47221