Theorem eldifsni 4794

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

Syntax hints:   → wi 4   ∈ wcel 2105   ≠ wne 2937   ∖ cdif 3959  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-v 3479  df-dif 3965  df-sn 4631

This theorem is referenced by:  eldifsnneq  4795  neldifsn  4796  suppssov1  8220  suppssov2  8221  suppss2  8223  suppssfv  8225  sniffsupp  9437  elfi2  9451  fifo  9469  en2other2  10046  finacn  10087  acndom2  10091  dfacacn  10179  kmlem11  10198  acncc  10477  axdc2lem  10485  1div0OLD  11920  expne0i  14131  incexc  15869  fprodn0f  16023  oddprm  16843  firest  17478  symgextf1lem  19452  pmtrmvd  19488  efgsp1  19769  efgredlem  19779  gsummpt1n0  19997  dprdfid  20051  dprdres  20062  dprd2da  20076  dmdprdsplit2lem  20079  ablfac1b  20104  ringelnzr  20539  isdomn4  20732  fidomndrnglem  20789  imadrhmcl  20814  sdrgacs  20818  cntzsdrg  20819  lvecinv  21132  lspsncmp  21135  lspsneq  21141  lspsneu  21142  lspdisjb  21145  lspexch  21148  lvecindp2  21158  cnflddiv  21430  uvcff  21828  frlmssuvc2  21832  frlmup2  21836  lindfrn  21858  f1lindf  21859  psrridm  22000  mplsubrg  22042  mplmon  22070  mplmonmul  22071  coe1tmmul  22295  dmatmul  22518  1marepvsma1  22604  mdetrsca2  22625  mdetrlin2  22628  mdetunilem5  22637  mdetunilem9  22641  maducoeval2  22661  gsummatr01lem3  22678  gsummatr01lem4  22679  gsummatr01  22680  cmpfi  23431  ptpjpre2  23603  alexsublem  24067  ptcmplem2  24076  divcn  24905  divcncf  25495  i1fmullem  25742  itg1addlem4  25747  itg1addlem4OLD  25748  itg1addlem5  25749  i1fmulc  25752  itg1mulc  25753  i1fres  25754  itg10a  25759  itg1climres  25763  mbfi1fseqlem4  25767  ellimc2  25926  dvcnp2  25969  dvcnp2OLD  25970  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvcobr  25997  dvcobrOLD  25998  dvcjbr  26001  dvrec  26007  dvrecg  26025  dvcnvlem  26028  dvexp3  26030  dveflem  26031  ftc1lem6  26096  deg1n0ima  26142  ig1peu  26228  plyeq0lem  26263  dgrlem  26282  dgrlb  26289  coemulhi  26307  fta1  26364  aannenlem2  26385  tayl0  26417  taylthlem2  26430  taylthlem2OLD  26431  abelthlem7  26496  dcubic  26903  rlimcnp  27022  efrlim  27026  efrlimOLD  27027  muinv  27250  logexprlim  27283  lgslem1  27355  lgsqr  27409  lgseisenlem2  27434  lgseisenlem4  27436  lgseisen  27437  lgsquadlem1  27438  lgsquad2  27444  m1lgs  27446  dchrisum0re  27571  dchrisum0lema  27572  dchrisum0lem2  27576  dchrisum0lem3  27577  nnne0s  28354  uhgrn0  29098  upgrn0  29120  upgrex  29123  numedglnl  29175  upgrreslem  29335  isuvtx  29426  cusgrexilem2  29473  cusgrexi  29474  structtocusgr  29477  cusgrfilem2  29488  frgrhash2wsp  30360  1div0apr  30496  fmptunsnop  32714  disjdsct  32717  pfxchn  32983  chnind  32984  elrgspnlem2  33232  elrgspnlem3  33233  domnprodn0  33261  isdrng4  33278  fracfld  33289  lindssn  33385  drngidl  33440  pidufd  33550  1arithufdlem3  33553  dfufd2  33557  zringidom  33558  zringfrac  33561  ig1pmindeg  33601  assafld  33664  irngnzply1  33705  irngnminplynz  33719  signstfvneq0  34565  lfuhgr2  35102  cusgredgex  35105  loop1cycl  35121  subfacp1lem1  35163  circum  35658  neibastop1  36341  bj-xpnzexb  36943  bj-restn0b  37073  curf  37584  poimirlem2  37608  poimirlem24  37630  poimirlem25  37631  dvtan  37656  ftc1cnnc  37678  ftc1anclem3  37681  rrndstprj2  37817  lsat0cv  39014  lkreqN  39151  lkrlspeqN  39152  dochnel  41375  djhcvat42  41397  dochsnkr  41454  dochsnkr2cl  41456  lcfl6lem  41480  lcfl8b  41486  lcfrlem16  41540  lcfrlem25  41549  lcfrlem27  41551  lcfrlem33  41557  lcfrlem37  41561  mapdn0  41651  mapdpglem24  41686  mapdindp1  41702  mapdhval2  41708  hdmap1val2  41782  hdmapnzcl  41827  hdmap14lem1  41850  hdmap14lem4a  41853  hdmap14lem6  41855  hgmaprnlem1N  41878  hdmapip1  41898  hgmapvvlem1  41905  hgmapvvlem2  41906  aks6d1c5lem2  42119  domnexpgn0cl  42509  prjspersym  42593  prjspreln0  42595  prjspvs  42596  dffltz  42620  aomclem2  43043  mpaaeu  43138  deg1mhm  43188  gneispace  44123  radcnvrat  44309  bccm1k  44337  disjf1o  45133  supminfxr2  45418  icoiccdif  45476  climrec  45558  climdivf  45567  lptre2pt  45595  0ellimcdiv  45604  limclner  45606  reclimc  45608  cnrefiisplem  45784  cncficcgt0  45843  fperdvper  45874  dvdivcncf  45882  dvnmul  45898  stoweidlem57  46012  dirkercncflem1  46058  fourierdlem24  46086  fourierdlem62  46123  fourierdlem66  46127  elaa2  46189  etransclem35  46224  etransclem47  46236  meadjiunlem  46420  ovnhoilem1  46556  hspmbllem1  46581  fmtnoprmfac1lem  47488  isubgruhgr  47791  isubgr0uhgr  47796  lindssnlvec  48331  logcxp0  48384