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

Theorem eldifsni 3888
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 3887 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
21simprbi 451 1  |-  ( A  e.  ( B  \  { C } )  ->  A  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721    =/= wne 2567    \ cdif 3277   {csn 3774
This theorem is referenced by:  neldifsn  3889  suppss2  6259  suppssfv  6260  suppssov1  6261  elfi2  7377  fifo  7395  finacn  7887  acndom2  7891  dfacacn  7977  kmlem11  7996  acncc  8276  axdc2lem  8284  1div0  9635  expne0i  11367  incexc  12572  oddprm  13144  firest  13615  efgsp1  15324  efgredlem  15334  dprdfid  15530  dprdres  15541  dprd2da  15555  dmdprdsplit2lem  15558  ablfac1b  15583  lvecinv  16140  lspsncmp  16143  lspsneq  16149  lspsneu  16150  lspdisjb  16153  lspexch  16156  lvecindp  16165  lvecindp2  16166  rngelnzr  16291  fidomndrnglem  16321  psrridm  16423  mvridlem  16438  mplsubrg  16458  mplmon  16481  mplmonmul  16482  mplcoe3  16484  mplcoe2  16485  coe1tmmul  16624  ptpjpre2  17565  ptcmplem2  18037  i1fmullem  19539  itg1addlem4  19544  itg1addlem5  19545  i1fmulc  19548  itg1mulc  19549  i1fres  19550  itg10a  19555  itg1climres  19559  mbfi1fseqlem4  19563  ellimc2  19717  dvcnp2  19759  dvaddbr  19777  dvmulbr  19778  dvcobr  19785  dvcjbr  19788  dvrec  19794  dvcnvlem  19813  dvexp3  19815  dveflem  19816  ftc1lem6  19878  evlslem3  19888  deg1n0ima  19965  ig1peu  20047  plyeq0lem  20082  dgrlem  20101  dgrlb  20108  coemulhi  20125  fta1  20178  aannenlem2  20199  tayl0  20231  taylthlem2  20243  abelthlem7  20307  dcubic  20639  rlimcnp  20757  efrlim  20761  muinv  20931  logexprlim  20962  lgslem1  21033  lgsqr  21083  lgseisenlem2  21087  lgseisenlem4  21089  lgseisen  21090  lgsquadlem1  21091  lgsquad2  21097  m1lgs  21099  dchrisum0re  21160  dchrisum0lema  21161  dchrisum0lem2  21165  dchrisum0lem3  21166  umgran0  21308  umgraex  21311  cusgraexi  21430  1div0apr  21715  suppss2f  24002  disjdsct  24043  subfacp1lem1  24818  circum  25064  ftc1cnnc  26178  neibastop1  26278  rrndstprj2  26430  aomclem2  27020  uvcresum  27110  frlmssuvc2  27115  frlmup2  27119  lindfrn  27159  f1lindf  27160  mpaaeu  27223  en2other2  27250  pmtrmvd  27266  mamulid  27326  mamurid  27327  sdrgacs  27377  cntzsdrg  27378  deg1mhm  27394  climrec  27596  climdivf  27605  stoweidlem57  27673  frghash2spot  28166  elogb  28246  lshpne0  29469  lsatcv0  29514  lsat0cv  29516  lkreqN  29653  lkrlspeqN  29654  dochnel  31876  djhcvat42  31898  dochsnkr  31955  dochsnkr2cl  31957  lcfl6lem  31981  lcfl8b  31987  lcfrlem16  32041  lcfrlem25  32050  lcfrlem27  32052  lcfrlem33  32058  lcfrlem37  32062  mapdn0  32152  mapdpglem24  32187  mapdindp1  32203  mapdhval2  32209  hdmap1val2  32284  hdmapnzcl  32331  hdmap14lem1  32354  hdmap14lem4a  32357  hdmap14lem6  32359  hgmaprnlem1N  32382  hdmapip1  32402  hgmapvvlem1  32409  hgmapvvlem2  32410
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-v 2918  df-dif 3283  df-sn 3780
  Copyright terms: Public domain W3C validator