Theorem eldifsni 4739

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

Syntax hints:   → wi 4   ∈ wcel 2111   ≠ wne 2928   ∖ cdif 3894  {csn 4573

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3900  df-sn 4574

This theorem is referenced by:  eldifsnneq  4740  neldifsn  4741  suppssov1  8127  suppssov2  8128  suppss2  8130  suppssfv  8132  sniffsupp  9284  elfi2  9298  fifo  9316  en2other2  9900  finacn  9941  acndom2  9945  dfacacn  10033  kmlem11  10052  acncc  10331  axdc2lem  10339  1div0OLD  11777  elfzodif0  13670  expne0i  14001  incexc  15744  fprodn0f  15898  oddprm  16722  firest  17336  pfxchn  18516  chnind  18527  chnccat  18532  chnrev  18533  symgextf1lem  19332  pmtrmvd  19368  efgsp1  19649  efgredlem  19659  gsummpt1n0  19877  dprdfid  19931  dprdres  19942  dprd2da  19956  dmdprdsplit2lem  19959  ablfac1b  19984  ringelnzr  20438  isdomn4  20631  fidomndrnglem  20687  imadrhmcl  20712  sdrgacs  20716  cntzsdrg  20717  lvecinv  21050  lspsncmp  21053  lspsneq  21059  lspsneu  21060  lspdisjb  21063  lspexch  21066  lvecindp2  21076  cnflddiv  21337  uvcff  21728  frlmssuvc2  21732  frlmup2  21736  lindfrn  21758  f1lindf  21759  psrridm  21900  mplsubrg  21942  mplmon  21970  mplmonmul  21971  coe1tmmul  22191  dmatmul  22412  1marepvsma1  22498  mdetrsca2  22519  mdetrlin2  22522  mdetunilem5  22531  mdetunilem9  22535  maducoeval2  22555  gsummatr01lem3  22572  gsummatr01lem4  22573  gsummatr01  22574  cmpfi  23323  ptpjpre2  23495  alexsublem  23959  ptcmplem2  23968  divcn  24786  divcncf  25375  i1fmullem  25622  itg1addlem4  25627  itg1addlem5  25628  i1fmulc  25631  itg1mulc  25632  i1fres  25633  itg10a  25638  itg1climres  25642  mbfi1fseqlem4  25646  ellimc2  25805  dvcnp2  25848  dvcnp2OLD  25849  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  dvcobr  25876  dvcobrOLD  25877  dvcjbr  25880  dvrec  25886  dvrecg  25904  dvcnvlem  25907  dvexp3  25909  dveflem  25910  ftc1lem6  25975  deg1n0ima  26021  ig1peu  26107  plyeq0lem  26142  dgrlem  26161  dgrlb  26168  coemulhi  26186  fta1  26243  aannenlem2  26264  tayl0  26296  taylthlem2  26309  taylthlem2OLD  26310  abelthlem7  26375  dcubic  26783  rlimcnp  26902  efrlim  26906  efrlimOLD  26907  muinv  27130  logexprlim  27163  lgslem1  27235  lgsqr  27289  lgseisenlem2  27314  lgseisenlem4  27316  lgseisen  27317  lgsquadlem1  27318  lgsquad2  27324  m1lgs  27326  dchrisum0re  27451  dchrisum0lema  27452  dchrisum0lem2  27456  dchrisum0lem3  27457  nnne0s  28265  uhgrn0  29045  upgrn0  29067  upgrex  29070  numedglnl  29122  upgrreslem  29282  isuvtx  29373  cusgrexilem2  29420  cusgrexi  29421  structtocusgr  29424  cusgrfilem2  29435  frgrhash2wsp  30312  1div0apr  30448  fmptunsnop  32681  disjdsct  32684  fxpsdrg  33144  elrgspnlem2  33210  elrgspnlem3  33211  domnprodn0  33242  isdrng4  33261  fracfld  33274  lindssn  33343  drngidl  33398  pidufd  33508  1arithufdlem3  33511  dfufd2  33515  zringidom  33516  zringfrac  33519  ig1pmindeg  33562  assafld  33650  irngnzply1  33704  irngnminplynz  33725  constrsdrg  33788  signstfvneq0  34585  lfuhgr2  35163  cusgredgex  35166  loop1cycl  35181  subfacp1lem1  35223  circum  35718  neibastop1  36403  bj-xpnzexb  37005  bj-restn0b  37135  curf  37637  poimirlem2  37661  poimirlem24  37683  poimirlem25  37684  dvtan  37709  ftc1cnnc  37731  ftc1anclem3  37734  rrndstprj2  37870  lsat0cv  39131  lkreqN  39268  lkrlspeqN  39269  dochnel  41491  djhcvat42  41513  dochsnkr  41570  dochsnkr2cl  41572  lcfl6lem  41596  lcfl8b  41602  lcfrlem16  41656  lcfrlem25  41665  lcfrlem27  41667  lcfrlem33  41673  lcfrlem37  41677  mapdn0  41767  mapdpglem24  41802  mapdindp1  41818  mapdhval2  41824  hdmap1val2  41898  hdmapnzcl  41943  hdmap14lem1  41966  hdmap14lem4a  41969  hdmap14lem6  41971  hgmaprnlem1N  41994  hdmapip1  42014  hgmapvvlem1  42021  hgmapvvlem2  42022  aks6d1c5lem2  42230  resuppsinopn  42455  readvcot  42456  domnexpgn0cl  42615  prjspersym  42699  prjspreln0  42701  prjspvs  42702  dffltz  42726  aomclem2  43147  mpaaeu  43242  deg1mhm  43292  gneispace  44226  radcnvrat  44406  bccm1k  44434  disjf1o  45287  supminfxr2  45566  icoiccdif  45623  climrec  45702  climdivf  45711  lptre2pt  45737  0ellimcdiv  45746  limclner  45748  reclimc  45750  cnrefiisplem  45926  cncficcgt0  45985  fperdvper  46016  dvdivcncf  46024  dvnmul  46040  stoweidlem57  46154  dirkercncflem1  46200  fourierdlem24  46228  fourierdlem62  46265  fourierdlem66  46269  elaa2  46331  etransclem35  46366  etransclem47  46378  meadjiunlem  46562  ovnhoilem1  46698  hspmbllem1  46723  fmtnoprmfac1lem  47663  isubgruhgr  47967  isubgr0uhgr  47972  lindssnlvec  48586  logcxp0  48635