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

Theorem eldifsni 3763
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 3762 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
21simprbi 450 1  |-  ( A  e.  ( B  \  { C } )  ->  A  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696    =/= wne 2459    \ cdif 3162   {csn 3653
This theorem is referenced by:  neldifsn  3764  suppss2  6089  suppssfv  6090  suppssov1  6091  fofinf1o  7153  elfi2  7184  fifo  7201  finacn  7693  acndom2  7697  dfacacn  7783  kmlem11  7802  acncc  8082  axdc2lem  8090  1div0  9441  xrsupss  10643  expne0i  11150  incexc  12312  oddprm  12884  firest  13353  efgsp1  15062  efgredlem  15072  dprdfid  15268  dprdres  15279  dprd2da  15293  dmdprdsplit2lem  15296  ablfac1b  15321  lvecinv  15882  lspsncmp  15885  lspsneq  15891  lspsneu  15892  lspdisjb  15895  lspexch  15898  lvecindp  15907  lvecindp2  15908  rngelnzr  16033  fidomndrnglem  16063  psrridm  16165  mvridlem  16180  mplsubrg  16200  mplmon  16223  mplmonmul  16224  mplcoe3  16226  mplcoe2  16227  coe1tmmul  16369  ptpjpre2  17291  ptcmplem2  17763  i1fmullem  19065  itg1addlem4  19070  itg1addlem5  19071  i1fmulc  19074  itg1mulc  19075  i1fres  19076  itg10a  19081  itg1climres  19085  mbfi1fseqlem4  19089  ellimc2  19243  dvcnp2  19285  dvaddbr  19303  dvmulbr  19304  dvcobr  19311  dvcjbr  19314  dvrec  19320  dvcnvlem  19339  dvexp3  19341  dveflem  19342  ftc1lem6  19404  evlslem3  19414  deg1n0ima  19491  ig1peu  19573  plyeq0lem  19608  dgrlem  19627  dgrlb  19634  coemulhi  19651  fta1  19704  aannenlem2  19725  tayl0  19757  taylthlem2  19769  abelthlem7  19830  dcubic  20158  rlimcnp  20276  efrlim  20280  muinv  20449  logexprlim  20480  lgslem1  20551  lgsqr  20601  lgseisenlem2  20605  lgseisenlem4  20607  lgseisen  20608  lgsquadlem1  20609  lgsquad2  20615  m1lgs  20617  dchrisum0re  20678  dchrisum0lema  20679  dchrisum0lem2  20683  dchrisum0lem3  20684  1div0apr  20857  suppss2f  23216  disjdsct  23384  dmgmseqn0  23711  subfacp1lem1  23725  umgran0  23887  umgraex  23890  circum  24022  ftc1cnnc  25025  neibastop1  26411  rrndstprj2  26658  aomclem2  27255  uvcresum  27345  frlmssuvc2  27350  frlmup2  27354  lindfrn  27394  f1lindf  27395  mpaaeu  27458  en2other2  27485  pmtrmvd  27501  mamulid  27561  mamurid  27562  sdrgacs  27612  cntzsdrg  27613  deg1mhm  27629  climrec  27832  climdivf  27841  stoweidlem57  27909  elogb  28513  lshpne0  29798  lsatcv0  29843  lsat0cv  29845  lkreqN  29982  lkrlspeqN  29983  dochnel  32205  djhcvat42  32227  dochsnkr  32284  dochsnkr2cl  32286  lcfl6lem  32310  lcfl8b  32316  lcfrlem16  32370  lcfrlem25  32379  lcfrlem27  32381  lcfrlem33  32387  lcfrlem37  32391  mapdn0  32481  mapdpglem24  32516  mapdindp1  32532  mapdhval2  32538  hdmap1val2  32613  hdmapnzcl  32660  hdmap14lem1  32683  hdmap14lem4a  32686  hdmap14lem6  32688  hgmaprnlem1N  32711  hdmapip1  32731  hgmapvvlem1  32738  hgmapvvlem2  32739
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-sn 3659
  Copyright terms: Public domain W3C validator