Theorem eldifsni 4734

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933   ∖ cdif 3887  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3432  df-dif 3893  df-sn 4569

This theorem is referenced by:  eldifsnneq  4735  neldifsn  4736  suppssov1  8144  suppssov2  8145  suppss2  8147  suppssfv  8149  sniffsupp  9310  elfi2  9324  fifo  9342  en2other2  9928  finacn  9969  acndom2  9973  dfacacn  10061  kmlem11  10080  acncc  10359  axdc2lem  10367  1div0OLD  11807  elfzodif0  13722  expne0i  14053  incexc  15799  fprodn0f  15953  oddprm  16778  firest  17392  pfxchn  18573  chnind  18584  chnccat  18589  chnrev  18590  symgextf1lem  19392  pmtrmvd  19428  efgsp1  19709  efgredlem  19719  gsummpt1n0  19937  dprdfid  19991  dprdres  20002  dprd2da  20016  dmdprdsplit2lem  20019  ablfac1b  20044  ringelnzr  20497  isdomn4  20690  fidomndrnglem  20746  imadrhmcl  20771  sdrgacs  20775  cntzsdrg  20776  lvecinv  21109  lspsncmp  21112  lspsneq  21118  lspsneu  21119  lspdisjb  21122  lspexch  21125  lvecindp2  21135  cnflddiv  21396  uvcff  21787  frlmssuvc2  21791  frlmup2  21795  lindfrn  21817  f1lindf  21818  psrridm  21957  mplsubrg  21999  mplmon  22029  mplmonmul  22030  coe1tmmul  22258  dmatmul  22478  1marepvsma1  22564  mdetrsca2  22585  mdetrlin2  22588  mdetunilem5  22597  mdetunilem9  22601  maducoeval2  22621  gsummatr01lem3  22638  gsummatr01lem4  22639  gsummatr01  22640  cmpfi  23389  ptpjpre2  23561  alexsublem  24025  ptcmplem2  24034  divcn  24851  divcncf  25430  i1fmullem  25677  itg1addlem4  25682  itg1addlem5  25683  i1fmulc  25686  itg1mulc  25687  i1fres  25688  itg10a  25693  itg1climres  25697  mbfi1fseqlem4  25701  ellimc2  25860  dvcnp2  25903  dvaddbr  25921  dvmulbr  25922  dvcobr  25929  dvcjbr  25932  dvrec  25938  dvrecg  25956  dvcnvlem  25959  dvexp3  25961  dveflem  25962  ftc1lem6  26024  deg1n0ima  26070  ig1peu  26156  plyeq0lem  26191  dgrlem  26210  dgrlb  26217  coemulhi  26235  fta1  26291  aannenlem2  26312  tayl0  26344  taylthlem2  26357  taylthlem2OLD  26358  abelthlem7  26422  dcubic  26829  rlimcnp  26948  efrlim  26952  efrlimOLD  26953  muinv  27176  logexprlim  27208  lgslem1  27280  lgsqr  27334  lgseisenlem2  27359  lgseisenlem4  27361  lgseisen  27362  lgsquadlem1  27363  lgsquad2  27369  m1lgs  27371  dchrisum0re  27496  dchrisum0lema  27497  dchrisum0lem2  27501  dchrisum0lem3  27502  nnne0s  28349  uhgrn0  29156  upgrn0  29178  upgrex  29181  numedglnl  29233  upgrreslem  29393  isuvtx  29484  cusgrexilem2  29531  cusgrexi  29532  structtocusgr  29535  cusgrfilem2  29546  frgrhash2wsp  30423  1div0apr  30559  fmptunsnop  32794  disjdsct  32797  fxpsdrg  33257  elrgspnlem2  33325  elrgspnlem3  33326  domnprodn0  33357  isdrng4  33377  fracfld  33390  lindssn  33459  drngidl  33514  pidufd  33624  1arithufdlem3  33627  dfufd2  33631  zringidom  33632  zringfrac  33635  deg1prod  33664  ig1pmindeg  33683  psrmonmul  33715  assafld  33803  irngnzply1  33857  irngnminplynz  33878  constrsdrg  33941  signstfvneq0  34738  lfuhgr2  35323  cusgredgex  35326  loop1cycl  35341  subfacp1lem1  35383  circum  35878  neibastop1  36563  bj-xpnzexb  37290  bj-restn0b  37425  curf  37941  poimirlem2  37965  poimirlem24  37987  poimirlem25  37988  dvtan  38013  ftc1cnnc  38035  ftc1anclem3  38038  rrndstprj2  38174  lsat0cv  39501  lkreqN  39638  lkrlspeqN  39639  dochnel  41861  djhcvat42  41883  dochsnkr  41940  dochsnkr2cl  41942  lcfl6lem  41966  lcfl8b  41972  lcfrlem16  42026  lcfrlem25  42035  lcfrlem27  42037  lcfrlem33  42043  lcfrlem37  42047  mapdn0  42137  mapdpglem24  42172  mapdindp1  42188  mapdhval2  42194  hdmap1val2  42268  hdmapnzcl  42313  hdmap14lem1  42336  hdmap14lem4a  42339  hdmap14lem6  42341  hgmaprnlem1N  42364  hdmapip1  42384  hgmapvvlem1  42391  hgmapvvlem2  42392  aks6d1c5lem2  42599  resuppsinopn  42817  readvcot  42818  domnexpgn0cl  42990  prjspersym  43062  prjspreln0  43064  prjspvs  43065  dffltz  43089  aomclem2  43509  mpaaeu  43604  deg1mhm  43654  gneispace  44587  radcnvrat  44767  bccm1k  44795  disjf1o  45647  supminfxr2  45923  icoiccdif  45980  climrec  46059  climdivf  46068  lptre2pt  46094  0ellimcdiv  46103  limclner  46105  reclimc  46107  cnrefiisplem  46283  cncficcgt0  46342  fperdvper  46373  dvdivcncf  46381  dvnmul  46397  stoweidlem57  46511  dirkercncflem1  46557  fourierdlem24  46585  fourierdlem62  46622  fourierdlem66  46626  elaa2  46688  etransclem35  46723  etransclem47  46735  meadjiunlem  46919  ovnhoilem1  47055  hspmbllem1  47080  fmtnoprmfac1lem  48047  isubgruhgr  48364  isubgr0uhgr  48369  lindssnlvec  48982  logcxp0  49031