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

Theorem eldifsni 4153
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 4152 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
21simprbi 464 1  |-  ( A  e.  ( B  \  { C } )  ->  A  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767    =/= wne 2662    \ cdif 3473   {csn 4027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3115  df-dif 3479  df-sn 4028
This theorem is referenced by:  neldifsn  4154  suppss2OLD  6514  suppssfvOLD  6515  suppssov1OLD  6516  suppssov1  6932  suppss2  6934  suppssfv  6936  sniffsupp  7869  elfi2  7874  fifo  7892  en2other2  8387  finacn  8431  acndom2  8435  dfacacn  8521  kmlem11  8540  acncc  8820  axdc2lem  8828  1div0  10208  expne0i  12166  incexc  13612  oddprm  14198  firest  14688  symgextf1lem  16250  pmtrmvd  16287  efgsp1  16561  efgredlem  16571  gsummpt1n0  16795  dprdfid  16859  dprdfidOLD  16866  dprdres  16877  dprd2da  16893  dmdprdsplit2lem  16896  ablfac1b  16923  lvecinv  17559  lspsncmp  17562  lspsneq  17568  lspsneu  17569  lspdisjb  17572  lspexch  17575  lvecindp  17584  lvecindp2  17585  rngelnzr  17713  fidomndrnglem  17754  psrridm  17857  psrridmOLD  17858  mvridlemOLD  17874  mplsubrg  17901  mplmon  17924  mplmonmul  17925  mplcoe3OLD  17928  mplcoe2OLD  17932  evlslem3  17982  coe1tmmul  18117  uvcff  18617  frlmssuvc2  18621  frlmssuvc2OLD  18623  frlmup2  18628  lindfrn  18651  f1lindf  18652  dmatmul  18794  1marepvsma1  18880  mdetrsca2  18901  mdetrlin2  18904  mdetunilem5  18913  mdetunilem9  18917  maducoeval2  18937  gsummatr01lem3  18954  gsummatr01lem4  18955  gsummatr01  18956  ptpjpre2  19844  ptcmplem2  20316  i1fmullem  21864  itg1addlem4  21869  itg1addlem5  21870  i1fmulc  21873  itg1mulc  21874  i1fres  21875  itg10a  21880  itg1climres  21884  mbfi1fseqlem4  21888  ellimc2  22044  dvcnp2  22086  dvaddbr  22104  dvmulbr  22105  dvcobr  22112  dvcjbr  22115  dvrec  22121  dvcnvlem  22140  dvexp3  22142  dveflem  22143  ftc1lem6  22205  deg1n0ima  22252  ig1peu  22335  plyeq0lem  22370  dgrlem  22389  dgrlb  22396  coemulhi  22413  fta1  22466  aannenlem2  22487  tayl0  22519  taylthlem2  22531  abelthlem7  22595  dcubic  22933  rlimcnp  23051  efrlim  23055  muinv  23225  logexprlim  23256  lgslem1  23327  lgsqr  23377  lgseisenlem2  23381  lgseisenlem4  23383  lgseisen  23384  lgsquadlem1  23385  lgsquad2  23391  m1lgs  23393  dchrisum0re  23454  dchrisum0lema  23455  dchrisum0lem2  23459  dchrisum0lem3  23460  umgran0  24024  umgraex  24027  cusgraexi  24172  frghash2spot  24768  1div0apr  24880  suppss2f  27178  disjdsct  27221  subfacp1lem1  28291  circum  28543  dvtan  29670  ftc1cnnc  29694  ftc1anclem3  29697  neibastop1  29808  rrndstprj2  29958  aomclem2  30633  mpaaeu  30732  sdrgacs  30783  cntzsdrg  30784  deg1mhm  30800  icoiccdif  31156  climrec  31173  climdivf  31182  lptre2pt  31210  0ellimcdiv  31219  limclner  31221  reclimc  31223  divcncf  31250  cncficcgt0  31255  dvrecg  31268  fperdvper  31276  dvdivcncf  31285  stoweidlem57  31385  dirkercncflem2  31432  fourierdlem24  31459  fourierdlem62  31497  fourierdlem66  31501  lindssnlvec  32186  elogb  32268  bj-xpnzexb  33617  lshpne0  33801  lsatcv0  33846  lsat0cv  33848  lkreqN  33985  lkrlspeqN  33986  dochnel  36208  djhcvat42  36230  dochsnkr  36287  dochsnkr2cl  36289  lcfl6lem  36313  lcfl8b  36319  lcfrlem16  36373  lcfrlem25  36382  lcfrlem27  36384  lcfrlem33  36390  lcfrlem37  36394  mapdn0  36484  mapdpglem24  36519  mapdindp1  36535  mapdhval2  36541  hdmap1val2  36616  hdmapnzcl  36663  hdmap14lem1  36686  hdmap14lem4a  36689  hdmap14lem6  36691  hgmaprnlem1N  36714  hdmapip1  36734  hgmapvvlem1  36741  hgmapvvlem2  36742
  Copyright terms: Public domain W3C validator