Theorem eldifsni 4815

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2946   ∖ cdif 3973  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-v 3490  df-dif 3979  df-sn 4649

This theorem is referenced by:  eldifsnneq  4816  neldifsn  4817  suppssov1  8238  suppssov2  8239  suppss2  8241  suppssfv  8243  sniffsupp  9469  elfi2  9483  fifo  9501  en2other2  10078  finacn  10119  acndom2  10123  dfacacn  10211  kmlem11  10230  acncc  10509  axdc2lem  10517  1div0OLD  11950  expne0i  14145  incexc  15885  fprodn0f  16039  oddprm  16857  firest  17492  symgextf1lem  19462  pmtrmvd  19498  efgsp1  19779  efgredlem  19789  gsummpt1n0  20007  dprdfid  20061  dprdres  20072  dprd2da  20086  dmdprdsplit2lem  20089  ablfac1b  20114  ringelnzr  20549  isdomn4  20738  fidomndrnglem  20795  imadrhmcl  20820  sdrgacs  20824  cntzsdrg  20825  lvecinv  21138  lspsncmp  21141  lspsneq  21147  lspsneu  21148  lspdisjb  21151  lspexch  21154  lvecindp2  21164  cnflddiv  21436  uvcff  21834  frlmssuvc2  21838  frlmup2  21842  lindfrn  21864  f1lindf  21865  psrridm  22006  mplsubrg  22048  mplmon  22076  mplmonmul  22077  coe1tmmul  22301  dmatmul  22524  1marepvsma1  22610  mdetrsca2  22631  mdetrlin2  22634  mdetunilem5  22643  mdetunilem9  22647  maducoeval2  22667  gsummatr01lem3  22684  gsummatr01lem4  22685  gsummatr01  22686  cmpfi  23437  ptpjpre2  23609  alexsublem  24073  ptcmplem2  24082  divcn  24911  divcncf  25501  i1fmullem  25748  itg1addlem4  25753  itg1addlem4OLD  25754  itg1addlem5  25755  i1fmulc  25758  itg1mulc  25759  i1fres  25760  itg10a  25765  itg1climres  25769  mbfi1fseqlem4  25773  ellimc2  25932  dvcnp2  25975  dvcnp2OLD  25976  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcobr  26003  dvcobrOLD  26004  dvcjbr  26007  dvrec  26013  dvrecg  26031  dvcnvlem  26034  dvexp3  26036  dveflem  26037  ftc1lem6  26102  deg1n0ima  26148  ig1peu  26234  plyeq0lem  26269  dgrlem  26288  dgrlb  26295  coemulhi  26313  fta1  26368  aannenlem2  26389  tayl0  26421  taylthlem2  26434  taylthlem2OLD  26435  abelthlem7  26500  dcubic  26907  rlimcnp  27026  efrlim  27030  efrlimOLD  27031  muinv  27254  logexprlim  27287  lgslem1  27359  lgsqr  27413  lgseisenlem2  27438  lgseisenlem4  27440  lgseisen  27441  lgsquadlem1  27442  lgsquad2  27448  m1lgs  27450  dchrisum0re  27575  dchrisum0lema  27576  dchrisum0lem2  27580  dchrisum0lem3  27581  nnne0s  28358  uhgrn0  29102  upgrn0  29124  upgrex  29127  numedglnl  29179  upgrreslem  29339  isuvtx  29430  cusgrexilem2  29477  cusgrexi  29478  structtocusgr  29481  cusgrfilem2  29492  frgrhash2wsp  30364  1div0apr  30500  disjdsct  32714  pfxchn  32982  chnind  32983  domnprodn0  33247  isdrng4  33264  fracfld  33275  lindssn  33371  drngidl  33426  pidufd  33536  1arithufdlem3  33539  dfufd2  33543  zringidom  33544  zringfrac  33547  ig1pmindeg  33587  assafld  33650  irngnzply1  33691  irngnminplynz  33705  signstfvneq0  34549  lfuhgr2  35086  cusgredgex  35089  loop1cycl  35105  subfacp1lem1  35147  circum  35642  neibastop1  36325  bj-xpnzexb  36927  bj-restn0b  37057  curf  37558  poimirlem2  37582  poimirlem24  37604  poimirlem25  37605  dvtan  37630  ftc1cnnc  37652  ftc1anclem3  37655  rrndstprj2  37791  lsat0cv  38989  lkreqN  39126  lkrlspeqN  39127  dochnel  41350  djhcvat42  41372  dochsnkr  41429  dochsnkr2cl  41431  lcfl6lem  41455  lcfl8b  41461  lcfrlem16  41515  lcfrlem25  41524  lcfrlem27  41526  lcfrlem33  41532  lcfrlem37  41536  mapdn0  41626  mapdpglem24  41661  mapdindp1  41677  mapdhval2  41683  hdmap1val2  41757  hdmapnzcl  41802  hdmap14lem1  41825  hdmap14lem4a  41828  hdmap14lem6  41830  hgmaprnlem1N  41853  hdmapip1  41873  hgmapvvlem1  41880  hgmapvvlem2  41881  aks6d1c5lem2  42095  domnexpgn0cl  42478  prjspersym  42562  prjspreln0  42564  prjspvs  42565  dffltz  42589  aomclem2  43012  mpaaeu  43107  deg1mhm  43161  gneispace  44096  radcnvrat  44283  bccm1k  44311  disjf1o  45098  supminfxr2  45384  icoiccdif  45442  climrec  45524  climdivf  45533  lptre2pt  45561  0ellimcdiv  45570  limclner  45572  reclimc  45574  cnrefiisplem  45750  cncficcgt0  45809  fperdvper  45840  dvdivcncf  45848  dvnmul  45864  stoweidlem57  45978  dirkercncflem1  46024  fourierdlem24  46052  fourierdlem62  46089  fourierdlem66  46093  elaa2  46155  etransclem35  46190  etransclem47  46202  meadjiunlem  46386  ovnhoilem1  46522  hspmbllem1  46547  fmtnoprmfac1lem  47438  isubgruhgr  47738  isubgr0uhgr  47743  lindssnlvec  48215  logcxp0  48269