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

Theorem eldifsni 3989
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 3988 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
21simprbi 461 1  |-  ( A  e.  ( B  \  { C } )  ->  A  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755    =/= wne 2596    \ cdif 3313   {csn 3865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-v 2964  df-dif 3319  df-sn 3866
This theorem is referenced by:  neldifsn  3990  suppss2OLD  6304  suppssfvOLD  6305  suppssov1OLD  6306  suppssov1  6710  suppss2  6712  suppssfv  6714  sniffsupp  7647  elfi2  7652  fifo  7670  en2other2  8164  finacn  8208  acndom2  8212  dfacacn  8298  kmlem11  8317  acncc  8597  axdc2lem  8605  1div0  9983  expne0i  11880  incexc  13283  oddprm  13865  firest  14354  symgextf1lem  15905  pmtrmvd  15942  efgsp1  16214  efgredlem  16224  gsummptif1n0  16431  dprdfid  16481  dprdfidOLD  16488  dprdres  16499  dprd2da  16515  dmdprdsplit2lem  16518  ablfac1b  16545  lvecinv  17116  lspsncmp  17119  lspsneq  17125  lspsneu  17126  lspdisjb  17129  lspexch  17132  lvecindp  17141  lvecindp2  17142  rngelnzr  17269  fidomndrnglem  17300  psrridm  17410  psrridmOLD  17411  mvridlemOLD  17426  mplsubrg  17453  mplmon  17476  mplmonmul  17477  mplcoe3OLD  17480  mplcoe2OLD  17482  coe1tmmul  17628  uvcff  18058  frlmssuvc2  18062  frlmssuvc2OLD  18064  frlmup2  18069  lindfrn  18092  f1lindf  18093  1marepvsma1  18236  mdetrsca2  18253  mdetrlin2  18255  mdetunilem5  18264  mdetunilem9  18268  maducoeval2  18288  gsummatr01lem3  18305  gsummatr01lem4  18306  gsummatr01  18307  ptpjpre2  18995  ptcmplem2  19467  i1fmullem  21014  itg1addlem4  21019  itg1addlem5  21020  i1fmulc  21023  itg1mulc  21024  i1fres  21025  itg10a  21030  itg1climres  21034  mbfi1fseqlem4  21038  ellimc2  21194  dvcnp2  21236  dvaddbr  21254  dvmulbr  21255  dvcobr  21262  dvcjbr  21265  dvrec  21271  dvcnvlem  21290  dvexp3  21292  dveflem  21293  ftc1lem6  21355  evlslem3  21366  deg1n0ima  21445  ig1peu  21528  plyeq0lem  21563  dgrlem  21582  dgrlb  21589  coemulhi  21606  fta1  21659  aannenlem2  21680  tayl0  21712  taylthlem2  21724  abelthlem7  21788  dcubic  22126  rlimcnp  22244  efrlim  22248  muinv  22418  logexprlim  22449  lgslem1  22520  lgsqr  22570  lgseisenlem2  22574  lgseisenlem4  22576  lgseisen  22577  lgsquadlem1  22578  lgsquad2  22584  m1lgs  22586  dchrisum0re  22647  dchrisum0lema  22648  dchrisum0lem2  22652  dchrisum0lem3  22653  umgran0  23077  umgraex  23080  cusgraexi  23199  1div0apr  23484  suppss2f  25778  disjdsct  25822  subfacp1lem1  26915  circum  27166  dvtan  28286  ftc1cnnc  28310  ftc1anclem3  28313  neibastop1  28424  rrndstprj2  28574  aomclem2  29253  mpaaeu  29352  sdrgacs  29403  cntzsdrg  29404  deg1mhm  29420  climrec  29622  climdivf  29631  stoweidlem57  29698  frghash2spot  30502  lindssnlvec  30729  elogb  30819  bj-xpnzexb  32036  lshpne0  32204  lsatcv0  32249  lsat0cv  32251  lkreqN  32388  lkrlspeqN  32389  dochnel  34611  djhcvat42  34633  dochsnkr  34690  dochsnkr2cl  34692  lcfl6lem  34716  lcfl8b  34722  lcfrlem16  34776  lcfrlem25  34785  lcfrlem27  34787  lcfrlem33  34793  lcfrlem37  34797  mapdn0  34887  mapdpglem24  34922  mapdindp1  34938  mapdhval2  34944  hdmap1val2  35019  hdmapnzcl  35066  hdmap14lem1  35089  hdmap14lem4a  35092  hdmap14lem6  35094  hgmaprnlem1N  35117  hdmapip1  35137  hgmapvvlem1  35144  hgmapvvlem2  35145
  Copyright terms: Public domain W3C validator