Theorem eldifsni 4792

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

Syntax hints:   → wi 4   ∈ wcel 2104   ≠ wne 2938   ∖ cdif 3944  {csn 4627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-v 3474  df-dif 3950  df-sn 4628

This theorem is referenced by:  eldifsnneq  4793  neldifsn  4794  suppssov1  8185  suppss2  8187  suppssfv  8189  sniffsupp  9397  elfi2  9411  fifo  9429  en2other2  10006  finacn  10047  acndom2  10051  dfacacn  10138  kmlem11  10157  acncc  10437  axdc2lem  10445  1div0  11877  expne0i  14064  incexc  15787  fprodn0f  15939  oddprm  16747  firest  17382  symgextf1lem  19329  pmtrmvd  19365  efgsp1  19646  efgredlem  19656  gsummpt1n0  19874  dprdfid  19928  dprdres  19939  dprd2da  19953  dmdprdsplit2lem  19956  ablfac1b  19981  ringelnzr  20412  imadrhmcl  20556  sdrgacs  20560  cntzsdrg  20561  lvecinv  20871  lspsncmp  20874  lspsneq  20880  lspsneu  20881  lspdisjb  20884  lspexch  20887  lvecindp2  20897  isdomn4  21118  fidomndrnglem  21125  uvcff  21565  frlmssuvc2  21569  frlmup2  21573  lindfrn  21595  f1lindf  21596  psrridm  21743  mplsubrg  21783  mplmon  21809  mplmonmul  21810  coe1tmmul  22019  dmatmul  22219  1marepvsma1  22305  mdetrsca2  22326  mdetrlin2  22329  mdetunilem5  22338  mdetunilem9  22342  maducoeval2  22362  gsummatr01lem3  22379  gsummatr01lem4  22380  gsummatr01  22381  cmpfi  23132  ptpjpre2  23304  alexsublem  23768  ptcmplem2  23777  divcn  24606  divcncf  25196  i1fmullem  25443  itg1addlem4  25448  itg1addlem4OLD  25449  itg1addlem5  25450  i1fmulc  25453  itg1mulc  25454  i1fres  25455  itg10a  25460  itg1climres  25464  mbfi1fseqlem4  25468  ellimc2  25626  dvcnp2  25669  dvcnp2OLD  25670  dvaddbr  25688  dvmulbr  25689  dvmulbrOLD  25690  dvcobr  25697  dvcobrOLD  25698  dvcjbr  25701  dvrec  25707  dvrecg  25725  dvcnvlem  25728  dvexp3  25730  dveflem  25731  ftc1lem6  25793  deg1n0ima  25842  ig1peu  25924  plyeq0lem  25959  dgrlem  25978  dgrlb  25985  coemulhi  26003  fta1  26057  aannenlem2  26078  tayl0  26110  taylthlem2  26122  abelthlem7  26186  dcubic  26587  rlimcnp  26706  efrlim  26710  muinv  26933  logexprlim  26964  lgslem1  27036  lgsqr  27090  lgseisenlem2  27115  lgseisenlem4  27117  lgseisen  27118  lgsquadlem1  27119  lgsquad2  27125  m1lgs  27127  dchrisum0re  27252  dchrisum0lema  27253  dchrisum0lem2  27257  dchrisum0lem3  27258  uhgrn0  28594  upgrn0  28616  upgrex  28619  numedglnl  28671  upgrreslem  28828  isuvtx  28919  cusgrexilem2  28966  cusgrexi  28967  structtocusgr  28970  cusgrfilem2  28980  frgrhash2wsp  29852  1div0apr  29988  disjdsct  32191  isdrng4  32665  lindssn  32768  drngidl  32825  ig1pmindeg  32947  irngnzply1  33044  irngnminplynz  33060  signstfvneq0  33881  lfuhgr2  34407  cusgredgex  34410  loop1cycl  34426  subfacp1lem1  34468  circum  34957  neibastop1  35547  bj-xpnzexb  36145  bj-restn0b  36275  curf  36769  poimirlem2  36793  poimirlem24  36815  poimirlem25  36816  dvtan  36841  ftc1cnnc  36863  ftc1anclem3  36866  rrndstprj2  37002  lsat0cv  38206  lkreqN  38343  lkrlspeqN  38344  dochnel  40567  djhcvat42  40589  dochsnkr  40646  dochsnkr2cl  40648  lcfl6lem  40672  lcfl8b  40678  lcfrlem16  40732  lcfrlem25  40741  lcfrlem27  40743  lcfrlem33  40749  lcfrlem37  40753  mapdn0  40843  mapdpglem24  40878  mapdindp1  40894  mapdhval2  40900  hdmap1val2  40974  hdmapnzcl  41019  hdmap14lem1  41042  hdmap14lem4a  41045  hdmap14lem6  41047  hgmaprnlem1N  41070  hdmapip1  41090  hgmapvvlem1  41097  hgmapvvlem2  41098  prjspersym  41651  prjspreln0  41653  prjspvs  41654  dffltz  41678  aomclem2  42099  mpaaeu  42194  deg1mhm  42251  gneispace  43187  radcnvrat  43375  bccm1k  43403  disjf1o  44188  supminfxr2  44477  icoiccdif  44535  climrec  44617  climdivf  44626  lptre2pt  44654  0ellimcdiv  44663  limclner  44665  reclimc  44667  cnrefiisplem  44843  cncficcgt0  44902  fperdvper  44933  dvdivcncf  44941  dvnmul  44957  stoweidlem57  45071  dirkercncflem1  45117  fourierdlem24  45145  fourierdlem62  45182  fourierdlem66  45186  elaa2  45248  etransclem35  45283  etransclem47  45295  meadjiunlem  45479  ovnhoilem1  45615  hspmbllem1  45640  fmtnoprmfac1lem  46530  lindssnlvec  47254  logcxp0  47308