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

Theorem eldifsni 3920
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 3919 . 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 1725    =/= wne 2598    \ cdif 3309   {csn 3806
This theorem is referenced by:  neldifsn  3921  suppss2  6292  suppssfv  6293  suppssov1  6294  elfi2  7411  fifo  7429  finacn  7923  acndom2  7927  dfacacn  8013  kmlem11  8032  acncc  8312  axdc2lem  8320  1div0  9671  expne0i  11404  incexc  12609  oddprm  13181  firest  13652  efgsp1  15361  efgredlem  15371  dprdfid  15567  dprdres  15578  dprd2da  15592  dmdprdsplit2lem  15595  ablfac1b  15620  lvecinv  16177  lspsncmp  16180  lspsneq  16186  lspsneu  16187  lspdisjb  16190  lspexch  16193  lvecindp  16202  lvecindp2  16203  rngelnzr  16328  fidomndrnglem  16358  psrridm  16460  mvridlem  16475  mplsubrg  16495  mplmon  16518  mplmonmul  16519  mplcoe3  16521  mplcoe2  16522  coe1tmmul  16661  ptpjpre2  17604  ptcmplem2  18076  i1fmullem  19578  itg1addlem4  19583  itg1addlem5  19584  i1fmulc  19587  itg1mulc  19588  i1fres  19589  itg10a  19594  itg1climres  19598  mbfi1fseqlem4  19602  ellimc2  19756  dvcnp2  19798  dvaddbr  19816  dvmulbr  19817  dvcobr  19824  dvcjbr  19827  dvrec  19833  dvcnvlem  19852  dvexp3  19854  dveflem  19855  ftc1lem6  19917  evlslem3  19927  deg1n0ima  20004  ig1peu  20086  plyeq0lem  20121  dgrlem  20140  dgrlb  20147  coemulhi  20164  fta1  20217  aannenlem2  20238  tayl0  20270  taylthlem2  20282  abelthlem7  20346  dcubic  20678  rlimcnp  20796  efrlim  20800  muinv  20970  logexprlim  21001  lgslem1  21072  lgsqr  21122  lgseisenlem2  21126  lgseisenlem4  21128  lgseisen  21129  lgsquadlem1  21130  lgsquad2  21136  m1lgs  21138  dchrisum0re  21199  dchrisum0lema  21200  dchrisum0lem2  21204  dchrisum0lem3  21205  umgran0  21347  umgraex  21350  cusgraexi  21469  1div0apr  21754  suppss2f  24041  disjdsct  24082  subfacp1lem1  24857  circum  25103  ftc1cnnc  26269  ftc1anclem3  26272  neibastop1  26379  rrndstprj2  26531  aomclem2  27121  uvcresum  27210  frlmssuvc2  27215  frlmup2  27219  lindfrn  27259  f1lindf  27260  mpaaeu  27323  en2other2  27350  pmtrmvd  27366  mamulid  27426  mamurid  27427  sdrgacs  27477  cntzsdrg  27478  deg1mhm  27494  climrec  27696  climdivf  27705  stoweidlem57  27773  frghash2spot  28389  elogb  28469  lshpne0  29721  lsatcv0  29766  lsat0cv  29768  lkreqN  29905  lkrlspeqN  29906  dochnel  32128  djhcvat42  32150  dochsnkr  32207  dochsnkr2cl  32209  lcfl6lem  32233  lcfl8b  32239  lcfrlem16  32293  lcfrlem25  32302  lcfrlem27  32304  lcfrlem33  32310  lcfrlem37  32314  mapdn0  32404  mapdpglem24  32439  mapdindp1  32455  mapdhval2  32461  hdmap1val2  32536  hdmapnzcl  32583  hdmap14lem1  32606  hdmap14lem4a  32609  hdmap14lem6  32611  hgmaprnlem1N  32634  hdmapip1  32654  hgmapvvlem1  32661  hgmapvvlem2  32662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-v 2950  df-dif 3315  df-sn 3812
  Copyright terms: Public domain W3C validator