Theorem eldifsni 4722

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 3016   ∖ cdif 3933  {csn 4567

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 2793

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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-v 3496  df-dif 3939  df-sn 4568

This theorem is referenced by:  eldifsnneq  4723  neldifsn  4725  suppssov1  7862  suppss2  7864  suppssfv  7866  sniffsupp  8873  elfi2  8878  fifo  8896  en2other2  9435  finacn  9476  acndom2  9480  dfacacn  9567  kmlem11  9586  acncc  9862  axdc2lem  9870  1div0  11299  expne0i  13462  incexc  15192  fprodn0f  15345  oddprm  16147  firest  16706  symgextf1lem  18548  pmtrmvd  18584  efgsp1  18863  efgredlem  18873  gsummpt1n0  19085  dprdfid  19139  dprdres  19150  dprd2da  19164  dmdprdsplit2lem  19167  ablfac1b  19192  sdrgacs  19580  cntzsdrg  19581  lvecinv  19885  lspsncmp  19888  lspsneq  19894  lspsneu  19895  lspdisjb  19898  lspexch  19901  lvecindp2  19911  ringelnzr  20039  fidomndrnglem  20079  psrridm  20184  mplsubrg  20220  mplmon  20244  mplmonmul  20245  coe1tmmul  20445  uvcff  20935  frlmssuvc2  20939  frlmup2  20943  lindfrn  20965  f1lindf  20966  dmatmul  21106  1marepvsma1  21192  mdetrsca2  21213  mdetrlin2  21216  mdetunilem5  21225  mdetunilem9  21229  maducoeval2  21249  gsummatr01lem3  21266  gsummatr01lem4  21267  gsummatr01  21268  cmpfi  22016  ptpjpre2  22188  alexsublem  22652  ptcmplem2  22661  divcncf  24048  i1fmullem  24295  itg1addlem4  24300  itg1addlem5  24301  i1fmulc  24304  itg1mulc  24305  i1fres  24306  itg10a  24311  itg1climres  24315  mbfi1fseqlem4  24319  ellimc2  24475  dvcnp2  24517  dvaddbr  24535  dvmulbr  24536  dvcobr  24543  dvcjbr  24546  dvrec  24552  dvrecg  24570  dvcnvlem  24573  dvexp3  24575  dveflem  24576  ftc1lem6  24638  deg1n0ima  24683  ig1peu  24765  plyeq0lem  24800  dgrlem  24819  dgrlb  24826  coemulhi  24844  fta1  24897  aannenlem2  24918  tayl0  24950  taylthlem2  24962  abelthlem7  25026  dcubic  25424  rlimcnp  25543  efrlim  25547  muinv  25770  logexprlim  25801  lgslem1  25873  lgsqr  25927  lgseisenlem2  25952  lgseisenlem4  25954  lgseisen  25955  lgsquadlem1  25956  lgsquad2  25962  m1lgs  25964  dchrisum0re  26089  dchrisum0lema  26090  dchrisum0lem2  26094  dchrisum0lem3  26095  uhgrn0  26852  upgrn0  26874  upgrex  26877  numedglnl  26929  upgrreslem  27086  isuvtx  27177  cusgrexilem2  27224  cusgrexi  27225  structtocusgr  27228  cusgrfilem2  27238  frgrhash2wsp  28111  1div0apr  28247  disjdsct  30438  lindssn  30939  signstfvneq0  31842  lfuhgr2  32365  cusgredgex  32368  loop1cycl  32384  subfacp1lem1  32426  circum  32917  neibastop1  33707  bj-xpnzexb  34276  bj-restn0b  34385  curf  34885  poimirlem2  34909  poimirlem24  34931  poimirlem25  34932  dvtan  34957  ftc1cnnc  34981  ftc1anclem3  34984  rrndstprj2  35124  lsat0cv  36184  lkreqN  36321  lkrlspeqN  36322  dochnel  38544  djhcvat42  38566  dochsnkr  38623  dochsnkr2cl  38625  lcfl6lem  38649  lcfl8b  38655  lcfrlem16  38709  lcfrlem25  38718  lcfrlem27  38720  lcfrlem33  38726  lcfrlem37  38730  mapdn0  38820  mapdpglem24  38855  mapdindp1  38871  mapdhval2  38877  hdmap1val2  38951  hdmapnzcl  38996  hdmap14lem1  39019  hdmap14lem4a  39022  hdmap14lem6  39024  hgmaprnlem1N  39047  hdmapip1  39067  hgmapvvlem1  39074  hgmapvvlem2  39075  prjspersym  39306  prjspreln0  39308  prjspvs  39309  dffltz  39320  aomclem2  39704  mpaaeu  39799  deg1mhm  39856  gneispace  40533  radcnvrat  40695  bccm1k  40723  disjf1o  41501  supminfxr2  41794  icoiccdif  41849  climrec  41933  climdivf  41942  lptre2pt  41970  0ellimcdiv  41979  limclner  41981  reclimc  41983  cnrefiisplem  42159  cncficcgt0  42220  fperdvper  42252  dvdivcncf  42261  dvnmul  42277  stoweidlem57  42391  dirkercncflem1  42437  fourierdlem24  42465  fourierdlem62  42502  fourierdlem66  42506  elaa2  42568  etransclem35  42603  etransclem47  42615  meadjiunlem  42796  ovnhoilem1  42932  hspmbllem1  42957  fmtnoprmfac1lem  43775  lindssnlvec  44590  logcxp0  44644