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

Theorem eldifn 3482
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 3341 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simprbi 464 1  |-  ( A  e.  ( B  \  C )  ->  -.  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1756    \ cdif 3328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-v 2977  df-dif 3334
This theorem is referenced by:  elndif  3483  noel  3644  disjel  3728  tz7.7  4748  funiunfv  5968  tfi  6467  peano5  6502  tz7.48-2  6900  tz7.49  6903  oaf1o  7005  undifixp  7302  domdifsn  7397  isinf  7529  ordtypelem7  7741  unxpwdom2  7806  inf3lem3  7839  infdifsn  7865  cantnfp1lem1  7889  cantnfp1lem3  7891  cantnflem1d  7899  cantnfp1lem1OLD  7915  cantnfp1lem3OLD  7917  cantnflem1dOLD  7922  setind  7957  fin23lem30  8514  domtriomlem  8614  axdc3lem4  8625  axdc4lem  8627  axcclem  8629  ttukeylem7  8687  konigthlem  8735  fpwwe2lem13  8812  fpwwe2  8813  hashf1lem1  12211  rlimrecl  13061  sumrblem  13191  fsumcvg  13192  summolem2a  13195  fsumss  13205  sumss2  13206  binomlem  13295  isumltss  13314  prmreclem2  13981  prmreclem5  13984  ramub1lem1  14090  efgs1b  16236  gsumzsplit  16421  gsumzsplitOLD  16422  gsum2d  16466  gsum2dOLD  16467  gsum2d2lem  16468  dmdprdsplitlem  16537  dmdprdsplitlemOLD  16538  pgpfac1lem1  16578  irredrmul  16802  lbsextlem2  17243  lbsextlem4  17245  psrlidm  17477  psrlidmOLD  17478  mplcoe1  17547  mplcoe5  17551  mplcoe2OLD  17553  evlslem3  17603  evlslem1  17604  cnsubrg  17876  maducoeval2  18449  madugsum  18452  elcls  18680  isclo  18694  ptbasfi  19157  ptopn2  19160  xkopt  19231  kqdisj  19308  fin1aufil  19508  ptcmplem4  19630  opnsubg  19681  tsmssplit  19729  zcld  20393  recld2  20394  reconnlem1  20406  ioombl1lem4  21045  i1fima2sn  21161  itg1val2  21165  i1f0  21168  itg1addlem4  21180  mbfi1flim  21204  itg2splitlem  21229  itg2split  21230  itg2cnlem1  21242  itg2cnlem2  21243  itgss2  21293  itgeqa  21294  itgss3  21295  itgless  21297  ibladdlem  21300  itgaddlem1  21303  iblabslem  21308  itggt0  21322  itgcn  21323  ply1termlem  21674  plypf1  21683  plyaddlem1  21684  plymullem1  21685  coeeulem  21695  coeidlem  21708  coeid3  21711  coefv0  21718  coemulc  21725  dvply1  21753  vieta1lem2  21780  aaliou2  21809  logdmnrp  22089  chpub  22562  chebbnd1lem1  22721  strlem1  25657  partfun  25996  elzdif0  26412  indval2  26474  ind0  26479  sigaclfu2  26567  eulerpartlemb  26754  regamcl  27050  lgam1  27053  gam1  27054  facgam  27055  prodrblem  27445  fprodcvg  27446  prodmolem2a  27450  fprodss  27464  fprodsplit  27479  dfon2lem6  27604  wfrlem10  27736  wfrlem13  27739  wfrlem16  27742  ibladdnclem  28451  itgaddnclem1  28453  iblabsnclem  28458  ftc1anclem5  28474  ftc1anclem6  28475  ftc1anclem8  28477  dvasin  28483  dvacos  28484  pridlc2  28875  pridlc3  28876  irrapx1  29172  pellqrex  29223  qirropth  29252  setindtr  29376  kelac1  29419  flcidc  29534  arearect  29594  areaquad  29595  stoweidlem34  29832  stoweidlem44  29842  stirlinglem5  29876
  Copyright terms: Public domain W3C validator