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

Theorem eldifsni 4089
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 4088 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
21simprbi 471 1  |-  ( A  e.  ( B  \  { C } )  ->  A  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1904    =/= wne 2641    \ cdif 3387   {csn 3959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-v 3033  df-dif 3393  df-sn 3960
This theorem is referenced by:  neldifsn  4090  suppssov1  6966  suppss2  6968  suppssfv  6970  sniffsupp  7941  elfi2  7946  fifo  7964  en2other2  8458  finacn  8499  acndom2  8503  dfacacn  8589  kmlem11  8608  acncc  8888  axdc2lem  8896  1div0  10293  expne0i  12342  incexc  13972  fprodn0f  14122  oddprm  14844  firest  15409  symgextf1lem  17139  pmtrmvd  17175  efgsp1  17465  efgredlem  17475  gsummpt1n0  17675  dprdfid  17728  dprdres  17739  dprd2da  17753  dmdprdsplit2lem  17756  ablfac1b  17781  lvecinv  18414  lspsncmp  18417  lspsneq  18423  lspsneu  18424  lspdisjb  18427  lspexch  18430  lvecindp  18439  lvecindp2  18440  ringelnzr  18567  fidomndrnglem  18607  psrridm  18705  mplsubrg  18741  mplmon  18764  mplmonmul  18765  evlslem3  18814  coe1tmmul  18947  uvcff  19426  frlmssuvc2  19430  frlmup2  19434  lindfrn  19456  f1lindf  19457  dmatmul  19599  1marepvsma1  19685  mdetrsca2  19706  mdetrlin2  19709  mdetunilem5  19718  mdetunilem9  19722  maducoeval2  19742  gsummatr01lem3  19759  gsummatr01lem4  19760  gsummatr01  19761  ptpjpre2  20672  ptcmplem2  21146  i1fmullem  22731  itg1addlem4  22736  itg1addlem5  22737  i1fmulc  22740  itg1mulc  22741  i1fres  22742  itg10a  22747  itg1climres  22751  mbfi1fseqlem4  22755  ellimc2  22911  dvcnp2  22953  dvaddbr  22971  dvmulbr  22972  dvcobr  22979  dvcjbr  22982  dvrec  22988  dvcnvlem  23007  dvexp3  23009  dveflem  23010  ftc1lem6  23072  deg1n0ima  23117  ig1peu  23201  ig1peuOLD  23202  plyeq0lem  23243  dgrlem  23262  dgrlb  23269  coemulhi  23287  fta1  23340  aannenlem2  23364  tayl0  23396  taylthlem2  23408  abelthlem7  23472  dcubic  23851  rlimcnp  23970  efrlim  23974  muinv  24201  logexprlim  24232  lgslem1  24303  lgsqr  24353  lgseisenlem2  24357  lgseisenlem4  24359  lgseisen  24360  lgsquadlem1  24361  lgsquad2  24367  m1lgs  24369  dchrisum0re  24430  dchrisum0lema  24431  dchrisum0lem2  24435  dchrisum0lem3  24436  umgran0  25126  umgraex  25129  cusgraexi  25275  frghash2spot  25870  1div0apr  25984  suppss2fOLD  28313  disjdsct  28358  signstfvneq0  29533  subfacp1lem1  29974  circum  30390  neibastop1  31086  bj-xpnzexb  31624  poimirlem2  32006  poimirlem24  32028  poimirlem25  32029  dvtan  32056  ftc1cnnc  32080  ftc1anclem3  32083  rrndstprj2  32227  lshpne0  32623  lsatcv0  32668  lsat0cv  32670  lkreqN  32807  lkrlspeqN  32808  dochnel  35032  djhcvat42  35054  dochsnkr  35111  dochsnkr2cl  35113  lcfl6lem  35137  lcfl8b  35143  lcfrlem16  35197  lcfrlem25  35206  lcfrlem27  35208  lcfrlem33  35214  lcfrlem37  35218  mapdn0  35308  mapdpglem24  35343  mapdindp1  35359  mapdhval2  35365  hdmap1val2  35440  hdmapnzcl  35487  hdmap14lem1  35510  hdmap14lem4a  35513  hdmap14lem6  35515  hgmaprnlem1N  35538  hdmapip1  35558  hgmapvvlem1  35565  hgmapvvlem2  35566  aomclem2  35984  mpaaeu  36087  sdrgacs  36138  cntzsdrg  36139  deg1mhm  36155  radcnvrat  36733  bccm1k  36761  disjf1o  37537  icoiccdif  37721  climrec  37778  climdivf  37789  lptre2pt  37817  0ellimcdiv  37827  limclner  37829  reclimc  37831  divcncf  37858  cncficcgt0  37863  dvrecg  37879  fperdvper  37887  dvdivcncf  37896  dvnmul  37915  stoweidlem57  38030  dirkercncflem1  38077  fourierdlem24  38105  fourierdlem62  38144  fourierdlem66  38148  elaa2  38211  etransclem35  38246  etransclem47  38258  meadjiunlem  38419  ovnhoilem1  38541  hspmbllem1  38566  uhgrn0  39311  upgrn0  39335  upgrex  39338  isuvtxa  39631  cusgrfilem2  39682  lindssnlvec  40787  logcxp0  40854
  Copyright terms: Public domain W3C validator