Theorem eldifsni 4756

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2957   ∖ cdif 3899  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3455  df-dif 3905  df-sn 4588

This theorem is used by:  eldifsnneq  4757  neldifsn  4758  suppssov1  8198  suppssov2  8199  suppss2  8201  suppssfv  8203  curf  8872  sniffsupp  9373  elfi2  9387  fifo  9405  en2other2  10015  finacn  10056  acndom2  10060  dfacacn  10147  kmlem11  10166  acncc  10445  axdc2lem  10453  elfzodif0  13828  expne0i  14160  incexc  15928  fprodn0f  16082  oddprm  16906  firest  17521  pfxchn  18702  chnind  18713  chnccat  18718  chnrev  18719  symgextf1lem  19548  pmtrmvd  19584  efgsp1  19865  efgredlem  19875  gsummpt1n0  20093  dprdfid  20147  dprdres  20158  dprd2da  20172  dmdprdsplit2lem  20175  ablfac1b  20200  ringelnzr  20685  isdomn4  20878  isdrng4  20903  fidomndrnglem  20940  imadrhmcl  20964  sdrgacs  20968  cntzsdrg  20969  lvecinv  21301  lspsncmp  21304  lspsneq  21310  lspsneu  21311  lspdisjb  21314  lspexch  21317  lvecindp2  21327  drngidl  21449  cnflddiv  21616  uvcff  22005  frlmssuvc2  22009  frlmup2  22013  lindfrn  22035  f1lindf  22036  psrridm  22178  mplsubrg  22220  mplmon  22252  mplmonmul  22253  coe1tmmul  22504  dmatmul  22720  1marepvsma1  22806  mdetrsca2  22827  mdetrlin2  22830  mdetunilem5  22839  mdetunilem9  22843  maducoeval2  22863  gsummatr01lem3  22880  gsummatr01lem4  22881  gsummatr01  22882  cmpfi  23634  ptpjpre2  23807  alexsublem  24271  ptcmplem2  24280  divcn  25097  divcncf  25676  i1fmullem  25923  itg1addlem4  25928  itg1addlem5  25929  i1fmulc  25932  itg1mulc  25933  i1fres  25934  itg10a  25939  itg1climres  25943  mbfi1fseqlem4  25947  ellimc2  26106  dvcnp2  26149  dvaddbr  26167  dvmulbr  26168  dvcobr  26175  dvcjbr  26178  dvrec  26184  dvrecg  26202  dvcnvlem  26205  dvexp3  26207  dveflem  26208  ftc1lem6  26270  deg1n0ima  26316  ig1peu  26402  plyeq0lem  26437  dgrlem  26456  dgrlb  26463  coemulhi  26481  fta1  26539  aannenlem2  26562  tayl0  26595  taylthlem2  26607  abelthlem7  26671  dcubic  27081  rlimcnp  27200  efrlim  27204  muinv  27427  logexprlim  27459  lgslem1  27531  lgsqr  27585  lgseisenlem2  27610  lgseisenlem4  27612  lgseisen  27613  lgsquadlem1  27614  lgsquad2  27620  m1lgs  27622  dchrisum0re  27747  dchrisum0lema  27748  dchrisum0lem2  27752  dchrisum0lem3  27753  nnne0s  28600  uhgrn0  29510  upgrn0  29532  upgrex  29535  numedglnl  29587  lfuhgr2  29592  upgrreslem  29750  isuvtx  29841  cusgrexilem2  29888  cusgrexi  29889  structtocusgr  29892  cusgrfilem2  29902  loop1cycl  30609  frgrhash2wsp  30798  1div0apr  30934  fmptunsnop  33159  disjdsct  33162  fxpsdrg  33602  elrgspnlem2  33670  elrgspnlem3  33671  domnprodn0  33705  fracfld  33736  lindssn  33798  pidufd  33940  1arithufdlem3  33943  dfufd2  33947  zringidom  33948  zringfrac  33951  deg1prod  33980  ig1pmindeg  33999  psrmonmul  34047  assafld  34134  irngnzply1  34188  irngnminplynz  34209  constrsdrg  34272  signstfvneq0  35067  cusgredgex  35707  subfacp1lem1  35745  circum  36240  neibastop1  36965  bj-xpnzexb  37692  bj-restn0b  37828  poimirlem2  38358  poimirlem24  38380  poimirlem25  38381  dvtan  38406  ftc1cnnc  38428  ftc1anclem3  38431  rrndstprj2  38568  lsat0cv  39893  lkreqN  40030  lkrlspeqN  40031  dochnel  42253  djhcvat42  42275  dochsnkr  42332  dochsnkr2cl  42334  lcfl6lem  42358  lcfl8b  42364  lcfrlem16  42418  lcfrlem25  42427  lcfrlem27  42429  lcfrlem33  42435  lcfrlem37  42439  mapdn0  42529  mapdpglem24  42564  mapdindp1  42580  mapdhval2  42586  hdmap1val2  42660  hdmapnzcl  42705  hdmap14lem1  42728  hdmap14lem4a  42731  hdmap14lem6  42733  hgmaprnlem1N  42756  hdmapip1  42776  hgmapvvlem1  42783  hgmapvvlem2  42784  aks6d1c5lem2  42991  resuppsinopn  43225  readvcot  43226  domnexpgn0cl  43392  prjspersym  43440  prjspreln0  43442  prjspvs  43443  dffltz  43467  aomclem2  43883  mpaaeu  43978  deg1mhm  44028  gneispace  44961  radcnvrat  45125  bccm1k  45153  disjf1o  46010  supminfxr2  46284  icoiccdif  46341  climrec  46420  climdivf  46429  lptre2pt  46455  0ellimcdiv  46464  limclner  46466  reclimc  46468  cnrefiisplem  46644  cncficcgt0  46703  fperdvper  46734  dvdivcncf  46742  dvnmul  46758  stoweidlem57  46872  dirkercncflem1  46918  fourierdlem24  46946  fourierdlem62  46983  fourierdlem66  46987  elaa2  47049  etransclem35  47084  etransclem47  47096  meadjiunlem  47280  ovnhoilem1  47416  hspmbllem1  47441  fmtnoprmfac1lem  48454  isubgruhgr  48771  isubgr0uhgr  48776  lindssnlvec  49403  logcxp0  49452