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

Theorem eldifsni 4141
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 4140 . 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 1804    =/= wne 2638    \ cdif 3458   {csn 4014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-v 3097  df-dif 3464  df-sn 4015
This theorem is referenced by:  neldifsn  4142  suppss2OLD  6515  suppssfvOLD  6516  suppssov1OLD  6517  suppssov1  6934  suppss2  6936  suppssfv  6938  sniffsupp  7871  elfi2  7876  fifo  7894  en2other2  8390  finacn  8434  acndom2  8438  dfacacn  8524  kmlem11  8543  acncc  8823  axdc2lem  8831  1div0  10215  expne0i  12180  incexc  13631  oddprm  14321  firest  14812  symgextf1lem  16424  pmtrmvd  16460  efgsp1  16734  efgredlem  16744  gsummpt1n0  16971  dprdfid  17036  dprdfidOLD  17043  dprdres  17054  dprd2da  17070  dmdprdsplit2lem  17073  ablfac1b  17100  lvecinv  17738  lspsncmp  17741  lspsneq  17747  lspsneu  17748  lspdisjb  17751  lspexch  17754  lvecindp  17763  lvecindp2  17764  ringelnzr  17893  fidomndrnglem  17934  psrridm  18037  psrridmOLD  18038  mvridlemOLD  18054  mplsubrg  18081  mplmon  18104  mplmonmul  18105  mplcoe3OLD  18108  mplcoe2OLD  18112  evlslem3  18162  coe1tmmul  18297  uvcff  18800  frlmssuvc2  18804  frlmssuvc2OLD  18806  frlmup2  18811  lindfrn  18834  f1lindf  18835  dmatmul  18977  1marepvsma1  19063  mdetrsca2  19084  mdetrlin2  19087  mdetunilem5  19096  mdetunilem9  19100  maducoeval2  19120  gsummatr01lem3  19137  gsummatr01lem4  19138  gsummatr01  19139  ptpjpre2  20059  ptcmplem2  20531  i1fmullem  22079  itg1addlem4  22084  itg1addlem5  22085  i1fmulc  22088  itg1mulc  22089  i1fres  22090  itg10a  22095  itg1climres  22099  mbfi1fseqlem4  22103  ellimc2  22259  dvcnp2  22301  dvaddbr  22319  dvmulbr  22320  dvcobr  22327  dvcjbr  22330  dvrec  22336  dvcnvlem  22355  dvexp3  22357  dveflem  22358  ftc1lem6  22420  deg1n0ima  22467  ig1peu  22550  plyeq0lem  22585  dgrlem  22604  dgrlb  22611  coemulhi  22629  fta1  22682  aannenlem2  22703  tayl0  22735  taylthlem2  22747  abelthlem7  22811  dcubic  23155  rlimcnp  23273  efrlim  23277  muinv  23447  logexprlim  23478  lgslem1  23549  lgsqr  23599  lgseisenlem2  23603  lgseisenlem4  23605  lgseisen  23606  lgsquadlem1  23607  lgsquad2  23613  m1lgs  23615  dchrisum0re  23676  dchrisum0lema  23677  dchrisum0lem2  23681  dchrisum0lem3  23682  umgran0  24298  umgraex  24301  cusgraexi  24446  frghash2spot  25041  1div0apr  25154  suppss2f  27455  disjdsct  27499  signstfvneq0  28507  subfacp1lem1  28601  circum  29018  dvtan  30041  ftc1cnnc  30065  ftc1anclem3  30068  neibastop1  30153  rrndstprj2  30303  aomclem2  30977  mpaaeu  31075  sdrgacs  31126  cntzsdrg  31127  deg1mhm  31143  radcnvrat  31171  icoiccdif  31518  fprodn0f  31548  climrec  31563  climdivf  31572  lptre2pt  31600  0ellimcdiv  31609  limclner  31611  reclimc  31613  divcncf  31640  cncficcgt0  31645  dvrecg  31661  fperdvper  31669  dvdivcncf  31678  dvnmul  31694  stoweidlem57  31793  dirkercncflem1  31839  fourierdlem24  31867  fourierdlem62  31905  fourierdlem66  31909  elaa2  31971  etransclem35  32006  etransclem47  32018  lindssnlvec  32957  elogb  33039  bj-xpnzexb  34401  lshpne0  34586  lsatcv0  34631  lsat0cv  34633  lkreqN  34770  lkrlspeqN  34771  dochnel  36995  djhcvat42  37017  dochsnkr  37074  dochsnkr2cl  37076  lcfl6lem  37100  lcfl8b  37106  lcfrlem16  37160  lcfrlem25  37169  lcfrlem27  37171  lcfrlem33  37177  lcfrlem37  37181  mapdn0  37271  mapdpglem24  37306  mapdindp1  37322  mapdhval2  37328  hdmap1val2  37403  hdmapnzcl  37450  hdmap14lem1  37473  hdmap14lem4a  37476  hdmap14lem6  37478  hgmaprnlem1N  37501  hdmapip1  37521  hgmapvvlem1  37528  hgmapvvlem2  37529
  Copyright terms: Public domain W3C validator