Theorem eldifsni 4741

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

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

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 3438  df-dif 3906  df-sn 4578

This theorem is referenced by:  eldifsnneq  4742  neldifsn  4743  suppssov1  8130  suppssov2  8131  suppss2  8133  suppssfv  8135  sniffsupp  9290  elfi2  9304  fifo  9322  en2other2  9903  finacn  9944  acndom2  9948  dfacacn  10036  kmlem11  10055  acncc  10334  axdc2lem  10342  1div0OLD  11780  expne0i  14001  incexc  15744  fprodn0f  15898  oddprm  16722  firest  17336  symgextf1lem  19299  pmtrmvd  19335  efgsp1  19616  efgredlem  19626  gsummpt1n0  19844  dprdfid  19898  dprdres  19909  dprd2da  19923  dmdprdsplit2lem  19926  ablfac1b  19951  ringelnzr  20408  isdomn4  20601  fidomndrnglem  20657  imadrhmcl  20682  sdrgacs  20686  cntzsdrg  20687  lvecinv  21020  lspsncmp  21023  lspsneq  21029  lspsneu  21030  lspdisjb  21033  lspexch  21036  lvecindp2  21046  cnflddiv  21307  uvcff  21698  frlmssuvc2  21702  frlmup2  21706  lindfrn  21728  f1lindf  21729  psrridm  21870  mplsubrg  21912  mplmon  21940  mplmonmul  21941  coe1tmmul  22161  dmatmul  22382  1marepvsma1  22468  mdetrsca2  22489  mdetrlin2  22492  mdetunilem5  22501  mdetunilem9  22505  maducoeval2  22525  gsummatr01lem3  22542  gsummatr01lem4  22543  gsummatr01  22544  cmpfi  23293  ptpjpre2  23465  alexsublem  23929  ptcmplem2  23938  divcn  24757  divcncf  25346  i1fmullem  25593  itg1addlem4  25598  itg1addlem5  25599  i1fmulc  25602  itg1mulc  25603  i1fres  25604  itg10a  25609  itg1climres  25613  mbfi1fseqlem4  25617  ellimc2  25776  dvcnp2  25819  dvcnp2OLD  25820  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  dvcobr  25847  dvcobrOLD  25848  dvcjbr  25851  dvrec  25857  dvrecg  25875  dvcnvlem  25878  dvexp3  25880  dveflem  25881  ftc1lem6  25946  deg1n0ima  25992  ig1peu  26078  plyeq0lem  26113  dgrlem  26132  dgrlb  26139  coemulhi  26157  fta1  26214  aannenlem2  26235  tayl0  26267  taylthlem2  26280  taylthlem2OLD  26281  abelthlem7  26346  dcubic  26754  rlimcnp  26873  efrlim  26877  efrlimOLD  26878  muinv  27101  logexprlim  27134  lgslem1  27206  lgsqr  27260  lgseisenlem2  27285  lgseisenlem4  27287  lgseisen  27288  lgsquadlem1  27289  lgsquad2  27295  m1lgs  27297  dchrisum0re  27422  dchrisum0lema  27423  dchrisum0lem2  27427  dchrisum0lem3  27428  nnne0s  28234  uhgrn0  29012  upgrn0  29034  upgrex  29037  numedglnl  29089  upgrreslem  29249  isuvtx  29340  cusgrexilem2  29387  cusgrexi  29388  structtocusgr  29391  cusgrfilem2  29402  frgrhash2wsp  30276  1div0apr  30412  fmptunsnop  32643  disjdsct  32646  elfzodif0  32738  pfxchn  32952  chnind  32954  fxpsdrg  33118  elrgspnlem2  33184  elrgspnlem3  33185  domnprodn0  33216  isdrng4  33235  fracfld  33248  lindssn  33316  drngidl  33371  pidufd  33481  1arithufdlem3  33484  dfufd2  33488  zringidom  33489  zringfrac  33492  ig1pmindeg  33535  assafld  33610  irngnzply1  33664  irngnminplynz  33685  constrsdrg  33748  signstfvneq0  34546  lfuhgr2  35102  cusgredgex  35105  loop1cycl  35120  subfacp1lem1  35162  circum  35657  neibastop1  36343  bj-xpnzexb  36945  bj-restn0b  37075  curf  37588  poimirlem2  37612  poimirlem24  37634  poimirlem25  37635  dvtan  37660  ftc1cnnc  37682  ftc1anclem3  37685  rrndstprj2  37821  lsat0cv  39022  lkreqN  39159  lkrlspeqN  39160  dochnel  41382  djhcvat42  41404  dochsnkr  41461  dochsnkr2cl  41463  lcfl6lem  41487  lcfl8b  41493  lcfrlem16  41547  lcfrlem25  41556  lcfrlem27  41558  lcfrlem33  41564  lcfrlem37  41568  mapdn0  41658  mapdpglem24  41693  mapdindp1  41709  mapdhval2  41715  hdmap1val2  41789  hdmapnzcl  41834  hdmap14lem1  41857  hdmap14lem4a  41860  hdmap14lem6  41862  hgmaprnlem1N  41885  hdmapip1  41905  hgmapvvlem1  41912  hgmapvvlem2  41913  aks6d1c5lem2  42121  resuppsinopn  42346  readvcot  42347  domnexpgn0cl  42506  prjspersym  42590  prjspreln0  42592  prjspvs  42593  dffltz  42617  aomclem2  43038  mpaaeu  43133  deg1mhm  43183  gneispace  44117  radcnvrat  44297  bccm1k  44325  disjf1o  45179  supminfxr2  45458  icoiccdif  45515  climrec  45594  climdivf  45603  lptre2pt  45631  0ellimcdiv  45640  limclner  45642  reclimc  45644  cnrefiisplem  45820  cncficcgt0  45879  fperdvper  45910  dvdivcncf  45918  dvnmul  45934  stoweidlem57  46048  dirkercncflem1  46094  fourierdlem24  46122  fourierdlem62  46159  fourierdlem66  46163  elaa2  46225  etransclem35  46260  etransclem47  46272  meadjiunlem  46456  ovnhoilem1  46592  hspmbllem1  46617  fmtnoprmfac1lem  47558  isubgruhgr  47862  isubgr0uhgr  47867  lindssnlvec  48481  logcxp0  48530