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

Theorem eldifn 3541
Description: Implication of membership in a class difference. (Contributed by NM, 3-May-1994.)
Assertion
Ref Expression
eldifn  |-  ( A  e.  ( B  \  C )  ->  -.  A  e.  C )

Proof of Theorem eldifn
StepHypRef Expression
1 eldif 3399 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simprbi 462 1  |-  ( A  e.  ( B  \  C )  ->  -.  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1826    \ cdif 3386
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-dif 3392
This theorem is referenced by:  elndif  3542  noel  3715  disjel  3789  tz7.7  4818  funiunfv  6061  tfi  6587  peano5  6622  tz7.48-2  7025  tz7.49  7028  oaf1o  7130  undifixp  7424  domdifsn  7519  isinf  7649  ordtypelem7  7864  unxpwdom2  7929  inf3lem3  7961  infdifsn  7987  cantnfp1lem1  8010  cantnfp1lem3  8012  cantnflem1d  8020  cantnfp1lem1OLD  8036  cantnfp1lem3OLD  8038  cantnflem1dOLD  8043  setind  8078  fin23lem30  8635  domtriomlem  8735  axdc3lem4  8746  axdc4lem  8748  axcclem  8750  ttukeylem7  8808  konigthlem  8856  fpwwe2lem13  8931  fpwwe2  8932  hashf1lem1  12408  rlimrecl  13405  sumrblem  13535  fsumcvg  13536  summolem2a  13539  fsumss  13549  sumss2  13550  binomlem  13643  isumltss  13662  prodrblem  13738  fprodcvg  13739  prodmolem2a  13743  fprodss  13757  fprodsplit  13772  prmreclem2  14437  prmreclem5  14440  ramub1lem1  14546  efgs1b  16871  gsumzsplit  17061  gsumzsplitOLD  17062  gsum2d  17113  gsum2dOLD  17114  gsum2d2lem  17115  dmdprdsplitlem  17197  dmdprdsplitlemOLD  17198  pgpfac1lem1  17238  irredrmul  17469  lbsextlem2  17918  lbsextlem4  17920  psrlidm  18169  psrlidmOLD  18170  mplcoe1  18240  mplcoe5  18244  mplcoe2OLD  18246  evlslem3  18296  evlslem1  18297  cnsubrg  18591  maducoeval2  19227  madugsum  19230  elcls  19660  isclo  19674  ptbasfi  20167  ptopn2  20170  xkopt  20241  kqdisj  20318  fin1aufil  20518  ptcmplem4  20640  opnsubg  20691  tsmssplit  20739  zcld  21403  recld2  21404  reconnlem1  21416  ioombl1lem4  22056  i1fima2sn  22172  itg1val2  22176  i1f0  22179  itg1addlem4  22191  mbfi1flim  22215  itg2splitlem  22240  itg2split  22241  itg2cnlem1  22253  itg2cnlem2  22254  itgss2  22304  itgeqa  22305  itgss3  22306  itgless  22308  ibladdlem  22311  itgaddlem1  22314  iblabslem  22319  itggt0  22333  itgcn  22334  ply1termlem  22685  plypf1  22694  plyaddlem1  22695  plymullem1  22696  coeeulem  22706  coeidlem  22719  coeid3  22722  coefv0  22730  coemulc  22737  dvply1  22765  vieta1lem2  22792  aaliou2  22821  logdmnrp  23109  chpub  23612  chebbnd1lem1  23771  strlem1  27285  partfun  27663  elzdif0  28114  indval2  28163  ind0  28168  sigaclfu2  28270  eulerpartlemb  28490  regamcl  28792  lgam1  28795  gam1  28796  facgam  28797  mrsubcn  29068  dfon2lem6  29385  wfrlem10  29517  wfrlem13  29520  wfrlem16  29523  ibladdnclem  30237  itgaddnclem1  30239  iblabsnclem  30244  ftc1anclem5  30260  ftc1anclem6  30261  ftc1anclem8  30263  dvasin  30269  dvacos  30270  pridlc2  30635  pridlc3  30636  irrapx1  30929  pellqrex  30980  qirropth  31009  setindtr  31132  kelac1  31175  flcidc  31291  arearect  31351  areaquad  31352  mccllem  31771  sumnnodd  31802  fprodcncf  31870  stoweidlem34  31982  stoweidlem44  31992  stirlinglem5  32026  fourierdlem62  32117  fouriersw  32180  elaa2lem  32182  etransclem44  32227
  Copyright terms: Public domain W3C validator