Theorem eldifsni 4757

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2926   ∖ cdif 3914  {csn 4592

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-v 3452  df-dif 3920  df-sn 4593

This theorem is referenced by:  eldifsnneq  4758  neldifsn  4759  suppssov1  8179  suppssov2  8180  suppss2  8182  suppssfv  8184  sniffsupp  9358  elfi2  9372  fifo  9390  en2other2  9969  finacn  10010  acndom2  10014  dfacacn  10102  kmlem11  10121  acncc  10400  axdc2lem  10408  1div0OLD  11845  expne0i  14066  incexc  15810  fprodn0f  15964  oddprm  16788  firest  17402  symgextf1lem  19357  pmtrmvd  19393  efgsp1  19674  efgredlem  19684  gsummpt1n0  19902  dprdfid  19956  dprdres  19967  dprd2da  19981  dmdprdsplit2lem  19984  ablfac1b  20009  ringelnzr  20439  isdomn4  20632  fidomndrnglem  20688  imadrhmcl  20713  sdrgacs  20717  cntzsdrg  20718  lvecinv  21030  lspsncmp  21033  lspsneq  21039  lspsneu  21040  lspdisjb  21043  lspexch  21046  lvecindp2  21056  cnflddiv  21319  uvcff  21707  frlmssuvc2  21711  frlmup2  21715  lindfrn  21737  f1lindf  21738  psrridm  21879  mplsubrg  21921  mplmon  21949  mplmonmul  21950  coe1tmmul  22170  dmatmul  22391  1marepvsma1  22477  mdetrsca2  22498  mdetrlin2  22501  mdetunilem5  22510  mdetunilem9  22514  maducoeval2  22534  gsummatr01lem3  22551  gsummatr01lem4  22552  gsummatr01  22553  cmpfi  23302  ptpjpre2  23474  alexsublem  23938  ptcmplem2  23947  divcn  24766  divcncf  25355  i1fmullem  25602  itg1addlem4  25607  itg1addlem5  25608  i1fmulc  25611  itg1mulc  25612  i1fres  25613  itg10a  25618  itg1climres  25622  mbfi1fseqlem4  25626  ellimc2  25785  dvcnp2  25828  dvcnp2OLD  25829  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvcobr  25856  dvcobrOLD  25857  dvcjbr  25860  dvrec  25866  dvrecg  25884  dvcnvlem  25887  dvexp3  25889  dveflem  25890  ftc1lem6  25955  deg1n0ima  26001  ig1peu  26087  plyeq0lem  26122  dgrlem  26141  dgrlb  26148  coemulhi  26166  fta1  26223  aannenlem2  26244  tayl0  26276  taylthlem2  26289  taylthlem2OLD  26290  abelthlem7  26355  dcubic  26763  rlimcnp  26882  efrlim  26886  efrlimOLD  26887  muinv  27110  logexprlim  27143  lgslem1  27215  lgsqr  27269  lgseisenlem2  27294  lgseisenlem4  27296  lgseisen  27297  lgsquadlem1  27298  lgsquad2  27304  m1lgs  27306  dchrisum0re  27431  dchrisum0lema  27432  dchrisum0lem2  27436  dchrisum0lem3  27437  nnne0s  28236  uhgrn0  29001  upgrn0  29023  upgrex  29026  numedglnl  29078  upgrreslem  29238  isuvtx  29329  cusgrexilem2  29376  cusgrexi  29377  structtocusgr  29380  cusgrfilem2  29391  frgrhash2wsp  30268  1div0apr  30404  fmptunsnop  32630  disjdsct  32633  elfzodif0  32724  pfxchn  32942  chnind  32944  elrgspnlem2  33201  elrgspnlem3  33202  domnprodn0  33233  isdrng4  33252  fracfld  33265  lindssn  33356  drngidl  33411  pidufd  33521  1arithufdlem3  33524  dfufd2  33528  zringidom  33529  zringfrac  33532  ig1pmindeg  33574  assafld  33640  irngnzply1  33693  irngnminplynz  33709  constrsdrg  33772  signstfvneq0  34570  lfuhgr2  35113  cusgredgex  35116  loop1cycl  35131  subfacp1lem1  35173  circum  35668  neibastop1  36354  bj-xpnzexb  36956  bj-restn0b  37086  curf  37599  poimirlem2  37623  poimirlem24  37645  poimirlem25  37646  dvtan  37671  ftc1cnnc  37693  ftc1anclem3  37696  rrndstprj2  37832  lsat0cv  39033  lkreqN  39170  lkrlspeqN  39171  dochnel  41394  djhcvat42  41416  dochsnkr  41473  dochsnkr2cl  41475  lcfl6lem  41499  lcfl8b  41505  lcfrlem16  41559  lcfrlem25  41568  lcfrlem27  41570  lcfrlem33  41576  lcfrlem37  41580  mapdn0  41670  mapdpglem24  41705  mapdindp1  41721  mapdhval2  41727  hdmap1val2  41801  hdmapnzcl  41846  hdmap14lem1  41869  hdmap14lem4a  41872  hdmap14lem6  41874  hgmaprnlem1N  41897  hdmapip1  41917  hgmapvvlem1  41924  hgmapvvlem2  41925  aks6d1c5lem2  42133  resuppsinopn  42358  readvcot  42359  domnexpgn0cl  42518  prjspersym  42602  prjspreln0  42604  prjspvs  42605  dffltz  42629  aomclem2  43051  mpaaeu  43146  deg1mhm  43196  gneispace  44130  radcnvrat  44310  bccm1k  44338  disjf1o  45192  supminfxr2  45472  icoiccdif  45529  climrec  45608  climdivf  45617  lptre2pt  45645  0ellimcdiv  45654  limclner  45656  reclimc  45658  cnrefiisplem  45834  cncficcgt0  45893  fperdvper  45924  dvdivcncf  45932  dvnmul  45948  stoweidlem57  46062  dirkercncflem1  46108  fourierdlem24  46136  fourierdlem62  46173  fourierdlem66  46177  elaa2  46239  etransclem35  46274  etransclem47  46286  meadjiunlem  46470  ovnhoilem1  46606  hspmbllem1  46631  fmtnoprmfac1lem  47569  isubgruhgr  47872  isubgr0uhgr  47877  lindssnlvec  48479  logcxp0  48528