Theorem eldifsni 4754

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925   ∖ cdif 3911  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3449  df-dif 3917  df-sn 4590

This theorem is referenced by:  eldifsnneq  4755  neldifsn  4756  suppssov1  8176  suppssov2  8177  suppss2  8179  suppssfv  8181  sniffsupp  9351  elfi2  9365  fifo  9383  en2other2  9962  finacn  10003  acndom2  10007  dfacacn  10095  kmlem11  10114  acncc  10393  axdc2lem  10401  1div0OLD  11838  expne0i  14059  incexc  15803  fprodn0f  15957  oddprm  16781  firest  17395  symgextf1lem  19350  pmtrmvd  19386  efgsp1  19667  efgredlem  19677  gsummpt1n0  19895  dprdfid  19949  dprdres  19960  dprd2da  19974  dmdprdsplit2lem  19977  ablfac1b  20002  ringelnzr  20432  isdomn4  20625  fidomndrnglem  20681  imadrhmcl  20706  sdrgacs  20710  cntzsdrg  20711  lvecinv  21023  lspsncmp  21026  lspsneq  21032  lspsneu  21033  lspdisjb  21036  lspexch  21039  lvecindp2  21049  cnflddiv  21312  uvcff  21700  frlmssuvc2  21704  frlmup2  21708  lindfrn  21730  f1lindf  21731  psrridm  21872  mplsubrg  21914  mplmon  21942  mplmonmul  21943  coe1tmmul  22163  dmatmul  22384  1marepvsma1  22470  mdetrsca2  22491  mdetrlin2  22494  mdetunilem5  22503  mdetunilem9  22507  maducoeval2  22527  gsummatr01lem3  22544  gsummatr01lem4  22545  gsummatr01  22546  cmpfi  23295  ptpjpre2  23467  alexsublem  23931  ptcmplem2  23940  divcn  24759  divcncf  25348  i1fmullem  25595  itg1addlem4  25600  itg1addlem5  25601  i1fmulc  25604  itg1mulc  25605  i1fres  25606  itg10a  25611  itg1climres  25615  mbfi1fseqlem4  25619  ellimc2  25778  dvcnp2  25821  dvcnp2OLD  25822  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvcobr  25849  dvcobrOLD  25850  dvcjbr  25853  dvrec  25859  dvrecg  25877  dvcnvlem  25880  dvexp3  25882  dveflem  25883  ftc1lem6  25948  deg1n0ima  25994  ig1peu  26080  plyeq0lem  26115  dgrlem  26134  dgrlb  26141  coemulhi  26159  fta1  26216  aannenlem2  26237  tayl0  26269  taylthlem2  26282  taylthlem2OLD  26283  abelthlem7  26348  dcubic  26756  rlimcnp  26875  efrlim  26879  efrlimOLD  26880  muinv  27103  logexprlim  27136  lgslem1  27208  lgsqr  27262  lgseisenlem2  27287  lgseisenlem4  27289  lgseisen  27290  lgsquadlem1  27291  lgsquad2  27297  m1lgs  27299  dchrisum0re  27424  dchrisum0lema  27425  dchrisum0lem2  27429  dchrisum0lem3  27430  nnne0s  28229  uhgrn0  28994  upgrn0  29016  upgrex  29019  numedglnl  29071  upgrreslem  29231  isuvtx  29322  cusgrexilem2  29369  cusgrexi  29370  structtocusgr  29373  cusgrfilem2  29384  frgrhash2wsp  30261  1div0apr  30397  fmptunsnop  32623  disjdsct  32626  elfzodif0  32717  pfxchn  32935  chnind  32937  elrgspnlem2  33194  elrgspnlem3  33195  domnprodn0  33226  isdrng4  33245  fracfld  33258  lindssn  33349  drngidl  33404  pidufd  33514  1arithufdlem3  33517  dfufd2  33521  zringidom  33522  zringfrac  33525  ig1pmindeg  33567  assafld  33633  irngnzply1  33686  irngnminplynz  33702  constrsdrg  33765  signstfvneq0  34563  lfuhgr2  35106  cusgredgex  35109  loop1cycl  35124  subfacp1lem1  35166  circum  35661  neibastop1  36347  bj-xpnzexb  36949  bj-restn0b  37079  curf  37592  poimirlem2  37616  poimirlem24  37638  poimirlem25  37639  dvtan  37664  ftc1cnnc  37686  ftc1anclem3  37689  rrndstprj2  37825  lsat0cv  39026  lkreqN  39163  lkrlspeqN  39164  dochnel  41387  djhcvat42  41409  dochsnkr  41466  dochsnkr2cl  41468  lcfl6lem  41492  lcfl8b  41498  lcfrlem16  41552  lcfrlem25  41561  lcfrlem27  41563  lcfrlem33  41569  lcfrlem37  41573  mapdn0  41663  mapdpglem24  41698  mapdindp1  41714  mapdhval2  41720  hdmap1val2  41794  hdmapnzcl  41839  hdmap14lem1  41862  hdmap14lem4a  41865  hdmap14lem6  41867  hgmaprnlem1N  41890  hdmapip1  41910  hgmapvvlem1  41917  hgmapvvlem2  41918  aks6d1c5lem2  42126  resuppsinopn  42351  readvcot  42352  domnexpgn0cl  42511  prjspersym  42595  prjspreln0  42597  prjspvs  42598  dffltz  42622  aomclem2  43044  mpaaeu  43139  deg1mhm  43189  gneispace  44123  radcnvrat  44303  bccm1k  44331  disjf1o  45185  supminfxr2  45465  icoiccdif  45522  climrec  45601  climdivf  45610  lptre2pt  45638  0ellimcdiv  45647  limclner  45649  reclimc  45651  cnrefiisplem  45827  cncficcgt0  45886  fperdvper  45917  dvdivcncf  45925  dvnmul  45941  stoweidlem57  46055  dirkercncflem1  46101  fourierdlem24  46129  fourierdlem62  46166  fourierdlem66  46170  elaa2  46232  etransclem35  46267  etransclem47  46279  meadjiunlem  46463  ovnhoilem1  46599  hspmbllem1  46624  fmtnoprmfac1lem  47565  isubgruhgr  47868  isubgr0uhgr  47873  lindssnlvec  48475  logcxp0  48524