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

Theorem eldifsni 4123
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 4122 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
21simprbi 465 1  |-  ( A  e.  ( B  \  { C } )  ->  A  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1868    =/= wne 2618    \ cdif 3433   {csn 3996
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-v 3083  df-dif 3439  df-sn 3997
This theorem is referenced by:  neldifsn  4124  suppssov1  6955  suppss2  6957  suppssfv  6959  sniffsupp  7926  elfi2  7931  fifo  7949  en2other2  8442  finacn  8482  acndom2  8486  dfacacn  8572  kmlem11  8591  acncc  8871  axdc2lem  8879  1div0  10272  expne0i  12304  incexc  13883  fprodn0f  14033  oddprm  14753  firest  15319  symgextf1lem  17049  pmtrmvd  17085  efgsp1  17375  efgredlem  17385  gsummpt1n0  17585  dprdfid  17638  dprdres  17649  dprd2da  17663  dmdprdsplit2lem  17666  ablfac1b  17691  lvecinv  18324  lspsncmp  18327  lspsneq  18333  lspsneu  18334  lspdisjb  18337  lspexch  18340  lvecindp  18349  lvecindp2  18350  ringelnzr  18478  fidomndrnglem  18518  psrridm  18616  mplsubrg  18652  mplmon  18675  mplmonmul  18676  evlslem3  18725  coe1tmmul  18858  uvcff  19336  frlmssuvc2  19340  frlmup2  19344  lindfrn  19366  f1lindf  19367  dmatmul  19509  1marepvsma1  19595  mdetrsca2  19616  mdetrlin2  19619  mdetunilem5  19628  mdetunilem9  19632  maducoeval2  19652  gsummatr01lem3  19669  gsummatr01lem4  19670  gsummatr01  19671  ptpjpre2  20582  ptcmplem2  21055  i1fmullem  22639  itg1addlem4  22644  itg1addlem5  22645  i1fmulc  22648  itg1mulc  22649  i1fres  22650  itg10a  22655  itg1climres  22659  mbfi1fseqlem4  22663  ellimc2  22819  dvcnp2  22861  dvaddbr  22879  dvmulbr  22880  dvcobr  22887  dvcjbr  22890  dvrec  22896  dvcnvlem  22915  dvexp3  22917  dveflem  22918  ftc1lem6  22980  deg1n0ima  23025  ig1peu  23109  ig1peuOLD  23110  plyeq0lem  23151  dgrlem  23170  dgrlb  23177  coemulhi  23195  fta1  23248  aannenlem2  23272  tayl0  23304  taylthlem2  23316  abelthlem7  23380  dcubic  23759  rlimcnp  23878  efrlim  23882  muinv  24109  logexprlim  24140  lgslem1  24211  lgsqr  24261  lgseisenlem2  24265  lgseisenlem4  24267  lgseisen  24268  lgsquadlem1  24269  lgsquad2  24275  m1lgs  24277  dchrisum0re  24338  dchrisum0lema  24339  dchrisum0lem2  24343  dchrisum0lem3  24344  umgran0  25034  umgraex  25037  cusgraexi  25182  frghash2spot  25777  1div0apr  25891  suppss2fOLD  28227  disjdsct  28273  signstfvneq0  29457  subfacp1lem1  29898  circum  30314  neibastop1  31008  bj-xpnzexb  31510  poimirlem2  31856  poimirlem24  31878  poimirlem25  31879  dvtan  31906  ftc1cnnc  31930  ftc1anclem3  31933  rrndstprj2  32077  lshpne0  32471  lsatcv0  32516  lsat0cv  32518  lkreqN  32655  lkrlspeqN  32656  dochnel  34880  djhcvat42  34902  dochsnkr  34959  dochsnkr2cl  34961  lcfl6lem  34985  lcfl8b  34991  lcfrlem16  35045  lcfrlem25  35054  lcfrlem27  35056  lcfrlem33  35062  lcfrlem37  35066  mapdn0  35156  mapdpglem24  35191  mapdindp1  35207  mapdhval2  35213  hdmap1val2  35288  hdmapnzcl  35335  hdmap14lem1  35358  hdmap14lem4a  35361  hdmap14lem6  35363  hgmaprnlem1N  35386  hdmapip1  35406  hgmapvvlem1  35413  hgmapvvlem2  35414  aomclem2  35833  mpaaeu  35936  sdrgacs  35987  cntzsdrg  35988  deg1mhm  36004  radcnvrat  36521  bccm1k  36549  disjf1o  37316  icoiccdif  37456  climrec  37501  climdivf  37512  lptre2pt  37540  0ellimcdiv  37550  limclner  37552  reclimc  37554  divcncf  37581  cncficcgt0  37586  dvrecg  37602  fperdvper  37610  dvdivcncf  37619  dvnmul  37638  stoweidlem57  37738  dirkercncflem1  37785  fourierdlem24  37813  fourierdlem62  37852  fourierdlem66  37856  elaa2  37919  etransclem35  37954  etransclem47  37966  meadjiunlem  38082  umgrn0  38842  umgrex  38845  lindssnlvec  39553  logcxp0  39620
  Copyright terms: Public domain W3C validator