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

Theorem eldifn 3476
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 3335 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simprbi 461 1  |-  ( A  e.  ( B  \  C )  ->  -.  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1761    \ cdif 3322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-dif 3328
This theorem is referenced by:  elndif  3477  noel  3638  disjel  3722  tz7.7  4741  funiunfv  5962  tfi  6463  peano5  6498  tz7.48-2  6893  tz7.49  6896  oaf1o  6998  undifixp  7295  domdifsn  7390  isinf  7522  ordtypelem7  7734  unxpwdom2  7799  inf3lem3  7832  infdifsn  7858  cantnfp1lem1  7882  cantnfp1lem3  7884  cantnflem1d  7892  cantnfp1lem1OLD  7908  cantnfp1lem3OLD  7910  cantnflem1dOLD  7915  setind  7950  fin23lem30  8507  domtriomlem  8607  axdc3lem4  8618  axdc4lem  8620  axcclem  8622  ttukeylem7  8680  konigthlem  8728  fpwwe2lem13  8805  fpwwe2  8806  hashf1lem1  12204  rlimrecl  13054  sumrblem  13184  fsumcvg  13185  summolem2a  13188  fsumss  13198  sumss2  13199  binomlem  13288  isumltss  13307  prmreclem2  13974  prmreclem5  13977  ramub1lem1  14083  efgs1b  16226  gsumzsplit  16411  gsumzsplitOLD  16412  gsum2d  16453  gsum2dOLD  16454  gsum2d2lem  16455  dmdprdsplitlem  16524  dmdprdsplitlemOLD  16525  pgpfac1lem1  16565  irredrmul  16789  lbsextlem2  17218  lbsextlem4  17220  psrlidm  17452  psrlidmOLD  17453  mplcoe1  17522  mplcoe2  17525  mplcoe2OLD  17526  evlslem3  17576  evlslem1  17577  cnsubrg  17832  maducoeval2  18405  madugsum  18408  elcls  18636  isclo  18650  ptbasfi  19113  ptopn2  19116  xkopt  19187  kqdisj  19264  fin1aufil  19464  ptcmplem4  19586  opnsubg  19637  tsmssplit  19685  zcld  20349  recld2  20350  reconnlem1  20362  ioombl1lem4  21001  i1fima2sn  21117  itg1val2  21121  i1f0  21124  itg1addlem4  21136  mbfi1flim  21160  itg2splitlem  21185  itg2split  21186  itg2cnlem1  21198  itg2cnlem2  21199  itgss2  21249  itgeqa  21250  itgss3  21251  itgless  21253  ibladdlem  21256  itgaddlem1  21259  iblabslem  21264  itggt0  21278  itgcn  21279  ply1termlem  21630  plypf1  21639  plyaddlem1  21640  plymullem1  21641  coeeulem  21651  coeidlem  21664  coeid3  21667  coefv0  21674  coemulc  21681  dvply1  21709  vieta1lem2  21736  aaliou2  21765  logdmnrp  22045  chpub  22518  chebbnd1lem1  22677  strlem1  25589  partfun  25928  elzdif0  26345  indval2  26407  ind0  26412  sigaclfu2  26500  eulerpartlemb  26681  regamcl  26977  lgam1  26980  gam1  26981  facgam  26982  prodrblem  27371  fprodcvg  27372  prodmolem2a  27376  fprodss  27390  fprodsplit  27405  dfon2lem6  27530  wfrlem10  27662  wfrlem13  27665  wfrlem16  27668  ibladdnclem  28373  itgaddnclem1  28375  iblabsnclem  28380  ftc1anclem5  28396  ftc1anclem6  28397  ftc1anclem8  28399  dvasin  28405  dvacos  28406  pridlc2  28797  pridlc3  28798  irrapx1  29094  pellqrex  29145  qirropth  29174  setindtr  29298  kelac1  29341  flcidc  29456  arearect  29516  areaquad  29517  stoweidlem34  29754  stoweidlem44  29764  stirlinglem5  29798
  Copyright terms: Public domain W3C validator