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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 3018   ∖ cdif 3935  {csn 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-v 3498  df-dif 3941  df-sn 4570

This theorem is referenced by:  eldifsnneq  4725  neldifsn  4727  suppssov1  7864  suppss2  7866  suppssfv  7868  sniffsupp  8875  elfi2  8880  fifo  8898  en2other2  9437  finacn  9478  acndom2  9482  dfacacn  9569  kmlem11  9588  acncc  9864  axdc2lem  9872  1div0  11301  expne0i  13464  incexc  15194  fprodn0f  15347  oddprm  16149  firest  16708  symgextf1lem  18550  pmtrmvd  18586  efgsp1  18865  efgredlem  18875  gsummpt1n0  19087  dprdfid  19141  dprdres  19152  dprd2da  19166  dmdprdsplit2lem  19169  ablfac1b  19194  sdrgacs  19582  cntzsdrg  19583  lvecinv  19887  lspsncmp  19890  lspsneq  19896  lspsneu  19897  lspdisjb  19900  lspexch  19903  lvecindp2  19913  ringelnzr  20041  fidomndrnglem  20081  psrridm  20186  mplsubrg  20222  mplmon  20246  mplmonmul  20247  coe1tmmul  20447  uvcff  20937  frlmssuvc2  20941  frlmup2  20945  lindfrn  20967  f1lindf  20968  dmatmul  21108  1marepvsma1  21194  mdetrsca2  21215  mdetrlin2  21218  mdetunilem5  21227  mdetunilem9  21231  maducoeval2  21251  gsummatr01lem3  21268  gsummatr01lem4  21269  gsummatr01  21270  cmpfi  22018  ptpjpre2  22190  alexsublem  22654  ptcmplem2  22663  divcncf  24050  i1fmullem  24297  itg1addlem4  24302  itg1addlem5  24303  i1fmulc  24306  itg1mulc  24307  i1fres  24308  itg10a  24313  itg1climres  24317  mbfi1fseqlem4  24321  ellimc2  24477  dvcnp2  24519  dvaddbr  24537  dvmulbr  24538  dvcobr  24545  dvcjbr  24548  dvrec  24554  dvrecg  24572  dvcnvlem  24575  dvexp3  24577  dveflem  24578  ftc1lem6  24640  deg1n0ima  24685  ig1peu  24767  plyeq0lem  24802  dgrlem  24821  dgrlb  24828  coemulhi  24846  fta1  24899  aannenlem2  24920  tayl0  24952  taylthlem2  24964  abelthlem7  25028  dcubic  25426  rlimcnp  25545  efrlim  25549  muinv  25772  logexprlim  25803  lgslem1  25875  lgsqr  25929  lgseisenlem2  25954  lgseisenlem4  25956  lgseisen  25957  lgsquadlem1  25958  lgsquad2  25964  m1lgs  25966  dchrisum0re  26091  dchrisum0lema  26092  dchrisum0lem2  26096  dchrisum0lem3  26097  uhgrn0  26854  upgrn0  26876  upgrex  26879  numedglnl  26931  upgrreslem  27088  isuvtx  27179  cusgrexilem2  27226  cusgrexi  27227  structtocusgr  27230  cusgrfilem2  27240  frgrhash2wsp  28113  1div0apr  28249  disjdsct  30440  lindssn  30941  signstfvneq0  31844  lfuhgr2  32367  cusgredgex  32370  loop1cycl  32386  subfacp1lem1  32428  circum  32919  neibastop1  33709  bj-xpnzexb  34275  bj-restn0b  34384  curf  34872  poimirlem2  34896  poimirlem24  34918  poimirlem25  34919  dvtan  34944  ftc1cnnc  34968  ftc1anclem3  34971  rrndstprj2  35111  lsat0cv  36171  lkreqN  36308  lkrlspeqN  36309  dochnel  38531  djhcvat42  38553  dochsnkr  38610  dochsnkr2cl  38612  lcfl6lem  38636  lcfl8b  38642  lcfrlem16  38696  lcfrlem25  38705  lcfrlem27  38707  lcfrlem33  38713  lcfrlem37  38717  mapdn0  38807  mapdpglem24  38842  mapdindp1  38858  mapdhval2  38864  hdmap1val2  38938  hdmapnzcl  38983  hdmap14lem1  39006  hdmap14lem4a  39009  hdmap14lem6  39011  hgmaprnlem1N  39034  hdmapip1  39054  hgmapvvlem1  39061  hgmapvvlem2  39062  prjspersym  39264  prjspreln0  39266  prjspvs  39267  dffltz  39278  aomclem2  39662  mpaaeu  39757  deg1mhm  39814  gneispace  40491  radcnvrat  40653  bccm1k  40681  disjf1o  41459  supminfxr2  41752  icoiccdif  41807  climrec  41891  climdivf  41900  lptre2pt  41928  0ellimcdiv  41937  limclner  41939  reclimc  41941  cnrefiisplem  42117  cncficcgt0  42178  fperdvper  42210  dvdivcncf  42219  dvnmul  42235  stoweidlem57  42349  dirkercncflem1  42395  fourierdlem24  42423  fourierdlem62  42460  fourierdlem66  42464  elaa2  42526  etransclem35  42561  etransclem47  42573  meadjiunlem  42754  ovnhoilem1  42890  hspmbllem1  42915  fmtnoprmfac1lem  43733  lindssnlvec  44548  logcxp0  44602