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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142   ≠ wne 2957   ∖ cdif 3901  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3456  df-dif 3907  df-sn 4589

This theorem is used by:  eldifsnneq  4758  neldifsn  4759  suppssov1  8191  suppssov2  8192  suppss2  8194  suppssfv  8196  sniffsupp  9358  elfi2  9372  fifo  9390  en2other2  10000  finacn  10041  acndom2  10045  dfacacn  10132  kmlem11  10151  acncc  10430  axdc2lem  10438  elfzodif0  13806  expne0i  14137  incexc  15898  fprodn0f  16052  oddprm  16876  firest  17491  pfxchn  18672  chnind  18683  chnccat  18688  chnrev  18689  symgextf1lem  19496  pmtrmvd  19532  efgsp1  19813  efgredlem  19823  gsummpt1n0  20041  dprdfid  20095  dprdres  20106  dprd2da  20120  dmdprdsplit2lem  20123  ablfac1b  20148  ringelnzr  20632  isdomn4  20825  isdrng4  20850  fidomndrnglem  20887  imadrhmcl  20911  sdrgacs  20915  cntzsdrg  20916  lvecinv  21248  lspsncmp  21251  lspsneq  21257  lspsneu  21258  lspdisjb  21261  lspexch  21264  lvecindp2  21274  drngidl  21396  cnflddiv  21563  uvcff  21952  frlmssuvc2  21956  frlmup2  21960  lindfrn  21982  f1lindf  21983  psrridm  22123  mplsubrg  22165  mplmon  22197  mplmonmul  22198  coe1tmmul  22449  dmatmul  22665  1marepvsma1  22751  mdetrsca2  22772  mdetrlin2  22775  mdetunilem5  22784  mdetunilem9  22788  maducoeval2  22808  gsummatr01lem3  22825  gsummatr01lem4  22826  gsummatr01  22827  cmpfi  23576  ptpjpre2  23748  alexsublem  24212  ptcmplem2  24221  divcn  25038  divcncf  25617  i1fmullem  25864  itg1addlem4  25869  itg1addlem5  25870  i1fmulc  25873  itg1mulc  25874  i1fres  25875  itg10a  25880  itg1climres  25884  mbfi1fseqlem4  25888  ellimc2  26047  dvcnp2  26090  dvaddbr  26108  dvmulbr  26109  dvcobr  26116  dvcjbr  26119  dvrec  26125  dvrecg  26143  dvcnvlem  26146  dvexp3  26148  dveflem  26149  ftc1lem6  26211  deg1n0ima  26257  ig1peu  26343  plyeq0lem  26378  dgrlem  26397  dgrlb  26404  coemulhi  26422  fta1  26480  aannenlem2  26503  tayl0  26536  taylthlem2  26548  abelthlem7  26612  dcubic  27022  rlimcnp  27141  efrlim  27145  muinv  27368  logexprlim  27400  lgslem1  27472  lgsqr  27526  lgseisenlem2  27551  lgseisenlem4  27553  lgseisen  27554  lgsquadlem1  27555  lgsquad2  27561  m1lgs  27563  dchrisum0re  27688  dchrisum0lema  27689  dchrisum0lem2  27693  dchrisum0lem3  27694  nnne0s  28541  uhgrn0  29428  upgrn0  29450  upgrex  29453  numedglnl  29505  upgrreslem  29665  isuvtx  29756  cusgrexilem2  29803  cusgrexi  29804  structtocusgr  29807  cusgrfilem2  29817  frgrhash2wsp  30694  1div0apr  30830  fmptunsnop  33056  disjdsct  33059  fxpsdrg  33504  elrgspnlem2  33572  elrgspnlem3  33573  domnprodn0  33607  fracfld  33638  lindssn  33700  pidufd  33842  1arithufdlem3  33845  dfufd2  33849  zringidom  33850  zringfrac  33853  deg1prod  33882  ig1pmindeg  33901  psrmonmul  33949  assafld  34036  irngnzply1  34090  irngnminplynz  34111  constrsdrg  34174  signstfvneq0  34968  lfuhgr2  35619  cusgredgex  35622  loop1cycl  35637  subfacp1lem1  35679  circum  36174  neibastop1  36898  bj-xpnzexb  37625  bj-restn0b  37761  curf  38277  poimirlem2  38301  poimirlem24  38323  poimirlem25  38324  dvtan  38349  ftc1cnnc  38371  ftc1anclem3  38374  rrndstprj2  38510  lsat0cv  39835  lkreqN  39972  lkrlspeqN  39973  dochnel  42195  djhcvat42  42217  dochsnkr  42274  dochsnkr2cl  42276  lcfl6lem  42300  lcfl8b  42306  lcfrlem16  42360  lcfrlem25  42369  lcfrlem27  42371  lcfrlem33  42377  lcfrlem37  42381  mapdn0  42471  mapdpglem24  42506  mapdindp1  42522  mapdhval2  42528  hdmap1val2  42602  hdmapnzcl  42647  hdmap14lem1  42670  hdmap14lem4a  42673  hdmap14lem6  42675  hgmaprnlem1N  42698  hdmapip1  42718  hgmapvvlem1  42725  hgmapvvlem2  42726  aks6d1c5lem2  42933  resuppsinopn  43152  readvcot  43153  domnexpgn0cl  43319  prjspersym  43367  prjspreln0  43369  prjspvs  43370  dffltz  43394  aomclem2  43810  mpaaeu  43905  deg1mhm  43955  gneispace  44888  radcnvrat  45052  bccm1k  45080  disjf1o  45937  supminfxr2  46211  icoiccdif  46268  climrec  46347  climdivf  46356  lptre2pt  46382  0ellimcdiv  46391  limclner  46393  reclimc  46395  cnrefiisplem  46571  cncficcgt0  46630  fperdvper  46661  dvdivcncf  46669  dvnmul  46685  stoweidlem57  46799  dirkercncflem1  46845  fourierdlem24  46873  fourierdlem62  46910  fourierdlem66  46914  elaa2  46976  etransclem35  47011  etransclem47  47023  meadjiunlem  47207  ovnhoilem1  47343  hspmbllem1  47368  fmtnoprmfac1lem  48344  isubgruhgr  48661  isubgr0uhgr  48666  lindssnlvec  49294  logcxp0  49343