MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eldifsni Structured version   Visualization version   Unicode version

Theorem eldifsni 4098
Description: Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
Assertion
Ref Expression
eldifsni  |-  ( A  e.  ( B  \  { C } )  ->  A  =/=  C )

Proof of Theorem eldifsni
StepHypRef Expression
1 eldifsn 4097 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
21simprbi 466 1  |-  ( A  e.  ( B  \  { C } )  ->  A  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1887    =/= wne 2622    \ cdif 3401   {csn 3968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-v 3047  df-dif 3407  df-sn 3969
This theorem is referenced by:  neldifsn  4099  suppssov1  6947  suppss2  6949  suppssfv  6951  sniffsupp  7923  elfi2  7928  fifo  7946  en2other2  8440  finacn  8481  acndom2  8485  dfacacn  8571  kmlem11  8590  acncc  8870  axdc2lem  8878  1div0  10271  expne0i  12304  incexc  13895  fprodn0f  14045  oddprm  14765  firest  15331  symgextf1lem  17061  pmtrmvd  17097  efgsp1  17387  efgredlem  17397  gsummpt1n0  17597  dprdfid  17650  dprdres  17661  dprd2da  17675  dmdprdsplit2lem  17678  ablfac1b  17703  lvecinv  18336  lspsncmp  18339  lspsneq  18345  lspsneu  18346  lspdisjb  18349  lspexch  18352  lvecindp  18361  lvecindp2  18362  ringelnzr  18490  fidomndrnglem  18530  psrridm  18628  mplsubrg  18664  mplmon  18687  mplmonmul  18688  evlslem3  18737  coe1tmmul  18870  uvcff  19349  frlmssuvc2  19353  frlmup2  19357  lindfrn  19379  f1lindf  19380  dmatmul  19522  1marepvsma1  19608  mdetrsca2  19629  mdetrlin2  19632  mdetunilem5  19641  mdetunilem9  19645  maducoeval2  19665  gsummatr01lem3  19682  gsummatr01lem4  19683  gsummatr01  19684  ptpjpre2  20595  ptcmplem2  21068  i1fmullem  22652  itg1addlem4  22657  itg1addlem5  22658  i1fmulc  22661  itg1mulc  22662  i1fres  22663  itg10a  22668  itg1climres  22672  mbfi1fseqlem4  22676  ellimc2  22832  dvcnp2  22874  dvaddbr  22892  dvmulbr  22893  dvcobr  22900  dvcjbr  22903  dvrec  22909  dvcnvlem  22928  dvexp3  22930  dveflem  22931  ftc1lem6  22993  deg1n0ima  23038  ig1peu  23122  ig1peuOLD  23123  plyeq0lem  23164  dgrlem  23183  dgrlb  23190  coemulhi  23208  fta1  23261  aannenlem2  23285  tayl0  23317  taylthlem2  23329  abelthlem7  23393  dcubic  23772  rlimcnp  23891  efrlim  23895  muinv  24122  logexprlim  24153  lgslem1  24224  lgsqr  24274  lgseisenlem2  24278  lgseisenlem4  24280  lgseisen  24281  lgsquadlem1  24282  lgsquad2  24288  m1lgs  24290  dchrisum0re  24351  dchrisum0lema  24352  dchrisum0lem2  24356  dchrisum0lem3  24357  umgran0  25047  umgraex  25050  cusgraexi  25196  frghash2spot  25791  1div0apr  25905  suppss2fOLD  28237  disjdsct  28283  signstfvneq0  29461  subfacp1lem1  29902  circum  30318  neibastop1  31015  bj-xpnzexb  31554  poimirlem2  31942  poimirlem24  31964  poimirlem25  31965  dvtan  31992  ftc1cnnc  32016  ftc1anclem3  32019  rrndstprj2  32163  lshpne0  32552  lsatcv0  32597  lsat0cv  32599  lkreqN  32736  lkrlspeqN  32737  dochnel  34961  djhcvat42  34983  dochsnkr  35040  dochsnkr2cl  35042  lcfl6lem  35066  lcfl8b  35072  lcfrlem16  35126  lcfrlem25  35135  lcfrlem27  35137  lcfrlem33  35143  lcfrlem37  35147  mapdn0  35237  mapdpglem24  35272  mapdindp1  35288  mapdhval2  35294  hdmap1val2  35369  hdmapnzcl  35416  hdmap14lem1  35439  hdmap14lem4a  35442  hdmap14lem6  35444  hgmaprnlem1N  35467  hdmapip1  35487  hgmapvvlem1  35494  hgmapvvlem2  35495  aomclem2  35913  mpaaeu  36016  sdrgacs  36067  cntzsdrg  36068  deg1mhm  36084  radcnvrat  36663  bccm1k  36691  disjf1o  37466  icoiccdif  37625  climrec  37681  climdivf  37692  lptre2pt  37720  0ellimcdiv  37730  limclner  37732  reclimc  37734  divcncf  37761  cncficcgt0  37766  dvrecg  37782  fperdvper  37790  dvdivcncf  37799  dvnmul  37818  stoweidlem57  37918  dirkercncflem1  37965  fourierdlem24  37993  fourierdlem62  38032  fourierdlem66  38036  elaa2  38099  etransclem35  38134  etransclem47  38146  meadjiunlem  38303  ovnhoilem1  38423  hspmbllem1  38448  uhgrn0  39158  upgrn0  39181  upgrex  39184  isuvtxa  39467  cusgrfilem2  39517  lindssnlvec  40332  logcxp0  40399
  Copyright terms: Public domain W3C validator