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

Theorem eldifsni 3872
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 3871 . 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 1717    =/= wne 2551    \ cdif 3261   {csn 3758
This theorem is referenced by:  neldifsn  3873  suppss2  6240  suppssfv  6241  suppssov1  6242  elfi2  7355  fifo  7373  finacn  7865  acndom2  7869  dfacacn  7955  kmlem11  7974  acncc  8254  axdc2lem  8262  1div0  9612  expne0i  11340  incexc  12545  oddprm  13117  firest  13588  efgsp1  15297  efgredlem  15307  dprdfid  15503  dprdres  15514  dprd2da  15528  dmdprdsplit2lem  15531  ablfac1b  15556  lvecinv  16113  lspsncmp  16116  lspsneq  16122  lspsneu  16123  lspdisjb  16126  lspexch  16129  lvecindp  16138  lvecindp2  16139  rngelnzr  16264  fidomndrnglem  16294  psrridm  16396  mvridlem  16411  mplsubrg  16431  mplmon  16454  mplmonmul  16455  mplcoe3  16457  mplcoe2  16458  coe1tmmul  16597  ptpjpre2  17534  ptcmplem2  18006  i1fmullem  19454  itg1addlem4  19459  itg1addlem5  19460  i1fmulc  19463  itg1mulc  19464  i1fres  19465  itg10a  19470  itg1climres  19474  mbfi1fseqlem4  19478  ellimc2  19632  dvcnp2  19674  dvaddbr  19692  dvmulbr  19693  dvcobr  19700  dvcjbr  19703  dvrec  19709  dvcnvlem  19728  dvexp3  19730  dveflem  19731  ftc1lem6  19793  evlslem3  19803  deg1n0ima  19880  ig1peu  19962  plyeq0lem  19997  dgrlem  20016  dgrlb  20023  coemulhi  20040  fta1  20093  aannenlem2  20114  tayl0  20146  taylthlem2  20158  abelthlem7  20222  dcubic  20554  rlimcnp  20672  efrlim  20676  muinv  20846  logexprlim  20877  lgslem1  20948  lgsqr  20998  lgseisenlem2  21002  lgseisenlem4  21004  lgseisen  21005  lgsquadlem1  21006  lgsquad2  21012  m1lgs  21014  dchrisum0re  21075  dchrisum0lema  21076  dchrisum0lem2  21080  dchrisum0lem3  21081  umgran0  21223  umgraex  21226  cusgraexi  21344  1div0apr  21611  suppss2f  23893  disjdsct  23932  subfacp1lem1  24645  circum  24891  ftc1cnnc  25980  neibastop1  26080  rrndstprj2  26232  aomclem2  26822  uvcresum  26912  frlmssuvc2  26917  frlmup2  26921  lindfrn  26961  f1lindf  26962  mpaaeu  27025  en2other2  27052  pmtrmvd  27068  mamulid  27128  mamurid  27129  sdrgacs  27179  cntzsdrg  27180  deg1mhm  27196  climrec  27398  climdivf  27407  stoweidlem57  27475  elogb  27879  lshpne0  29102  lsatcv0  29147  lsat0cv  29149  lkreqN  29286  lkrlspeqN  29287  dochnel  31509  djhcvat42  31531  dochsnkr  31588  dochsnkr2cl  31590  lcfl6lem  31614  lcfl8b  31620  lcfrlem16  31674  lcfrlem25  31683  lcfrlem27  31685  lcfrlem33  31691  lcfrlem37  31695  mapdn0  31785  mapdpglem24  31820  mapdindp1  31836  mapdhval2  31842  hdmap1val2  31917  hdmapnzcl  31964  hdmap14lem1  31987  hdmap14lem4a  31990  hdmap14lem6  31992  hgmaprnlem1N  32015  hdmapip1  32035  hgmapvvlem1  32042  hgmapvvlem2  32043
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-v 2902  df-dif 3267  df-sn 3764
  Copyright terms: Public domain W3C validator