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

Theorem eldifn 3612
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 3471 . 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 1804    \ cdif 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-dif 3464
This theorem is referenced by:  elndif  3613  noel  3774  disjel  3859  tz7.7  4894  funiunfv  6145  tfi  6673  peano5  6708  tz7.48-2  7109  tz7.49  7112  oaf1o  7214  undifixp  7507  domdifsn  7602  isinf  7735  ordtypelem7  7952  unxpwdom2  8017  inf3lem3  8050  infdifsn  8076  cantnfp1lem1  8100  cantnfp1lem3  8102  cantnflem1d  8110  cantnfp1lem1OLD  8126  cantnfp1lem3OLD  8128  cantnflem1dOLD  8133  setind  8168  fin23lem30  8725  domtriomlem  8825  axdc3lem4  8836  axdc4lem  8838  axcclem  8840  ttukeylem7  8898  konigthlem  8946  fpwwe2lem13  9023  fpwwe2  9024  hashf1lem1  12483  rlimrecl  13382  sumrblem  13512  fsumcvg  13513  summolem2a  13516  fsumss  13526  sumss2  13527  binomlem  13620  isumltss  13639  prmreclem2  14312  prmreclem5  14315  ramub1lem1  14421  efgs1b  16628  gsumzsplit  16818  gsumzsplitOLD  16819  gsum2d  16873  gsum2dOLD  16874  gsum2d2lem  16875  dmdprdsplitlem  16958  dmdprdsplitlemOLD  16959  pgpfac1lem1  16999  irredrmul  17230  lbsextlem2  17679  lbsextlem4  17681  psrlidm  17930  psrlidmOLD  17931  mplcoe1  18001  mplcoe5  18005  mplcoe2OLD  18007  evlslem3  18057  evlslem1  18058  cnsubrg  18352  maducoeval2  19015  madugsum  19018  elcls  19447  isclo  19461  ptbasfi  19955  ptopn2  19958  xkopt  20029  kqdisj  20106  fin1aufil  20306  ptcmplem4  20428  opnsubg  20479  tsmssplit  20527  zcld  21191  recld2  21192  reconnlem1  21204  ioombl1lem4  21844  i1fima2sn  21960  itg1val2  21964  i1f0  21967  itg1addlem4  21979  mbfi1flim  22003  itg2splitlem  22028  itg2split  22029  itg2cnlem1  22041  itg2cnlem2  22042  itgss2  22092  itgeqa  22093  itgss3  22094  itgless  22096  ibladdlem  22099  itgaddlem1  22102  iblabslem  22107  itggt0  22121  itgcn  22122  ply1termlem  22473  plypf1  22482  plyaddlem1  22483  plymullem1  22484  coeeulem  22494  coeidlem  22507  coeid3  22510  coefv0  22517  coemulc  22524  dvply1  22552  vieta1lem2  22579  aaliou2  22608  logdmnrp  22894  chpub  23367  chebbnd1lem1  23526  strlem1  27041  partfun  27388  elzdif0  27834  indval2  27901  ind0  27906  sigaclfu2  27994  eulerpartlemb  28180  regamcl  28476  lgam1  28479  gam1  28480  facgam  28481  mrsubcn  28752  prodrblem  29036  fprodcvg  29037  prodmolem2a  29041  fprodss  29055  fprodsplit  29070  dfon2lem6  29195  wfrlem10  29327  wfrlem13  29330  wfrlem16  29333  ibladdnclem  30046  itgaddnclem1  30048  iblabsnclem  30053  ftc1anclem5  30069  ftc1anclem6  30070  ftc1anclem8  30072  dvasin  30078  dvacos  30079  pridlc2  30444  pridlc3  30445  irrapx1  30739  pellqrex  30790  qirropth  30819  setindtr  30941  kelac1  30984  flcidc  31099  arearect  31159  areaquad  31160  sumnnodd  31544  stoweidlem34  31705  stoweidlem44  31715  stirlinglem5  31749  fourierdlem62  31840  fouriersw  31903
  Copyright terms: Public domain W3C validator