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

Theorem eldifn 3430
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 3290 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simprbi 451 1  |-  ( A  e.  ( B  \  C )  ->  -.  A  e.  C )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1721    \ cdif 3277
This theorem is referenced by:  elndif  3431  noel  3592  disjel  3634  tz7.7  4567  tfi  4792  peano5  4827  funiunfv  5954  tz7.48-2  6658  tz7.49  6661  oaf1o  6765  undifixp  7057  domdifsn  7150  isinf  7281  ordtypelem7  7449  unxpwdom2  7512  inf3lem3  7541  infdifsn  7567  cantnfp1lem1  7590  cantnfp1lem3  7592  cantnflem1d  7600  setind  7629  fin23lem30  8178  domtriomlem  8278  axdc3lem4  8289  axdc4lem  8291  axcclem  8293  ttukeylem7  8351  konigthlem  8399  fpwwe2lem13  8473  fpwwe2  8474  hashf1lem1  11659  rlimrecl  12329  sumrblem  12460  fsumcvg  12461  summolem2a  12464  fsumss  12474  sumss2  12475  binomlem  12563  isumltss  12583  prmreclem2  13240  prmreclem5  13243  ramub1lem1  13349  efgs1b  15323  gsumzsplit  15484  gsum2d  15501  gsum2d2lem  15502  dmdprdsplitlem  15550  pgpfac1lem1  15587  irredrmul  15767  lbsextlem2  16186  lbsextlem4  16188  psrlidm  16422  mplcoe1  16483  mplcoe2  16485  cnsubrg  16714  elcls  17092  isclo  17106  ptbasfi  17566  ptopn2  17569  xkopt  17640  kqdisj  17717  fin1aufil  17917  ptcmplem4  18039  opnsubg  18090  tsmssplit  18134  zcld  18797  recld2  18798  reconnlem1  18810  ioombl1lem4  19408  i1fima2sn  19525  itg1val2  19529  i1f0  19532  itg1addlem4  19544  mbfi1flim  19568  itg2splitlem  19593  itg2split  19594  itg2cnlem1  19606  itg2cnlem2  19607  itgss2  19657  itgeqa  19658  itgss3  19659  itgless  19661  ibladdlem  19664  itgaddlem1  19667  iblabslem  19672  itggt0  19686  itgcn  19687  evlslem3  19888  evlslem1  19889  ply1termlem  20075  plypf1  20084  plyaddlem1  20085  plymullem1  20086  coeeulem  20096  coeidlem  20109  coeid3  20112  coefv0  20119  coemulc  20126  dvply1  20154  vieta1lem2  20181  aaliou2  20210  logdmnrp  20485  chpub  20957  chebbnd1lem1  21116  strlem1  23706  partfun  24040  elzdif0  24317  indval2  24365  ind0  24370  sigaclfu2  24457  regamcl  24798  lgam1  24801  gam1  24802  facgam  24803  prodrblem  25208  fprodcvg  25209  prodmolem2a  25213  fprodss  25227  fprodsplit  25242  dfon2lem6  25358  wfrlem10  25479  wfrlem13  25482  wfrlem16  25485  ibladdnclem  26160  itgaddnclem1  26162  iblabsnclem  26167  dvreasin  26179  pridlc2  26572  pridlc3  26573  irrapx1  26781  pellqrex  26832  qirropth  26861  setindtr  26985  kelac1  27029  flcidc  27247  stoweidlem34  27650  stoweidlem44  27660  stirlinglem5  27694
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-dif 3283
  Copyright terms: Public domain W3C validator