Theorem eldifsni 4795

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

Syntax hints:   → wi 4   ∈ wcel 2098   ≠ wne 2929   ∖ cdif 3941  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-v 3463  df-dif 3947  df-sn 4631

This theorem is referenced by:  eldifsnneq  4796  neldifsn  4797  suppssov1  8203  suppssov2  8204  suppss2  8206  suppssfv  8208  sniffsupp  9425  elfi2  9439  fifo  9457  en2other2  10034  finacn  10075  acndom2  10079  dfacacn  10166  kmlem11  10185  acncc  10465  axdc2lem  10473  1div0OLD  11906  expne0i  14095  incexc  15819  fprodn0f  15971  oddprm  16782  firest  17417  symgextf1lem  19387  pmtrmvd  19423  efgsp1  19704  efgredlem  19714  gsummpt1n0  19932  dprdfid  19986  dprdres  19997  dprd2da  20011  dmdprdsplit2lem  20014  ablfac1b  20039  ringelnzr  20472  imadrhmcl  20697  sdrgacs  20701  cntzsdrg  20702  lvecinv  21013  lspsncmp  21016  lspsneq  21022  lspsneu  21023  lspdisjb  21026  lspexch  21029  lvecindp2  21039  isdomn4  21267  fidomndrnglem  21277  cnflddiv  21345  uvcff  21742  frlmssuvc2  21746  frlmup2  21750  lindfrn  21772  f1lindf  21773  psrridm  21925  mplsubrg  21967  mplmon  21995  mplmonmul  21996  coe1tmmul  22221  dmatmul  22443  1marepvsma1  22529  mdetrsca2  22550  mdetrlin2  22553  mdetunilem5  22562  mdetunilem9  22566  maducoeval2  22586  gsummatr01lem3  22603  gsummatr01lem4  22604  gsummatr01  22605  cmpfi  23356  ptpjpre2  23528  alexsublem  23992  ptcmplem2  24001  divcn  24830  divcncf  25420  i1fmullem  25667  itg1addlem4  25672  itg1addlem4OLD  25673  itg1addlem5  25674  i1fmulc  25677  itg1mulc  25678  i1fres  25679  itg10a  25684  itg1climres  25688  mbfi1fseqlem4  25692  ellimc2  25850  dvcnp2  25893  dvcnp2OLD  25894  dvaddbr  25912  dvmulbr  25913  dvmulbrOLD  25914  dvcobr  25921  dvcobrOLD  25922  dvcjbr  25925  dvrec  25931  dvrecg  25949  dvcnvlem  25952  dvexp3  25954  dveflem  25955  ftc1lem6  26020  deg1n0ima  26069  ig1peu  26154  plyeq0lem  26189  dgrlem  26208  dgrlb  26215  coemulhi  26233  fta1  26288  aannenlem2  26309  tayl0  26341  taylthlem2  26354  taylthlem2OLD  26355  abelthlem7  26420  dcubic  26823  rlimcnp  26942  efrlim  26946  efrlimOLD  26947  muinv  27170  logexprlim  27203  lgslem1  27275  lgsqr  27329  lgseisenlem2  27354  lgseisenlem4  27356  lgseisen  27357  lgsquadlem1  27358  lgsquad2  27364  m1lgs  27366  dchrisum0re  27491  dchrisum0lema  27492  dchrisum0lem2  27496  dchrisum0lem3  27497  nnne0s  28257  uhgrn0  28952  upgrn0  28974  upgrex  28977  numedglnl  29029  upgrreslem  29189  isuvtx  29280  cusgrexilem2  29327  cusgrexi  29328  structtocusgr  29331  cusgrfilem2  29342  frgrhash2wsp  30214  1div0apr  30350  disjdsct  32564  domnprodn0  33065  isdrng4  33083  fracfld  33094  lindssn  33190  drngidl  33245  pidufd  33358  1arithufdlem3  33361  dfufd2  33365  zringidom  33366  zringfrac  33369  ig1pmindeg  33403  irngnzply1  33500  irngnminplynz  33513  signstfvneq0  34335  lfuhgr2  34859  cusgredgex  34862  loop1cycl  34878  subfacp1lem1  34920  circum  35409  neibastop1  35974  bj-xpnzexb  36571  bj-restn0b  36701  curf  37202  poimirlem2  37226  poimirlem24  37248  poimirlem25  37249  dvtan  37274  ftc1cnnc  37296  ftc1anclem3  37299  rrndstprj2  37435  lsat0cv  38635  lkreqN  38772  lkrlspeqN  38773  dochnel  40996  djhcvat42  41018  dochsnkr  41075  dochsnkr2cl  41077  lcfl6lem  41101  lcfl8b  41107  lcfrlem16  41161  lcfrlem25  41170  lcfrlem27  41172  lcfrlem33  41178  lcfrlem37  41182  mapdn0  41272  mapdpglem24  41307  mapdindp1  41323  mapdhval2  41329  hdmap1val2  41403  hdmapnzcl  41448  hdmap14lem1  41471  hdmap14lem4a  41474  hdmap14lem6  41476  hgmaprnlem1N  41499  hdmapip1  41519  hgmapvvlem1  41526  hgmapvvlem2  41527  aks6d1c5lem2  41741  prjspersym  42166  prjspreln0  42168  prjspvs  42169  dffltz  42193  aomclem2  42621  mpaaeu  42716  deg1mhm  42770  gneispace  43706  radcnvrat  43893  bccm1k  43921  disjf1o  44703  supminfxr2  44989  icoiccdif  45047  climrec  45129  climdivf  45138  lptre2pt  45166  0ellimcdiv  45175  limclner  45177  reclimc  45179  cnrefiisplem  45355  cncficcgt0  45414  fperdvper  45445  dvdivcncf  45453  dvnmul  45469  stoweidlem57  45583  dirkercncflem1  45629  fourierdlem24  45657  fourierdlem62  45694  fourierdlem66  45698  elaa2  45760  etransclem35  45795  etransclem47  45807  meadjiunlem  45991  ovnhoilem1  46127  hspmbllem1  46152  fmtnoprmfac1lem  47041  isubgruhgr  47338  isubgr0uhgr  47343  lindssnlvec  47740  logcxp0  47794