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

Theorem eldifn 3462
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 3322 . 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 1725    \ cdif 3309
This theorem is referenced by:  elndif  3463  noel  3624  disjel  3666  tz7.7  4599  tfi  4824  peano5  4859  funiunfv  5986  tz7.48-2  6690  tz7.49  6693  oaf1o  6797  undifixp  7089  domdifsn  7182  isinf  7313  ordtypelem7  7482  unxpwdom2  7545  inf3lem3  7574  infdifsn  7600  cantnfp1lem1  7623  cantnfp1lem3  7625  cantnflem1d  7633  setind  7662  fin23lem30  8211  domtriomlem  8311  axdc3lem4  8322  axdc4lem  8324  axcclem  8326  ttukeylem7  8384  konigthlem  8432  fpwwe2lem13  8506  fpwwe2  8507  hashf1lem1  11692  rlimrecl  12362  sumrblem  12493  fsumcvg  12494  summolem2a  12497  fsumss  12507  sumss2  12508  binomlem  12596  isumltss  12616  prmreclem2  13273  prmreclem5  13276  ramub1lem1  13382  efgs1b  15356  gsumzsplit  15517  gsum2d  15534  gsum2d2lem  15535  dmdprdsplitlem  15583  pgpfac1lem1  15620  irredrmul  15800  lbsextlem2  16219  lbsextlem4  16221  psrlidm  16455  mplcoe1  16516  mplcoe2  16518  cnsubrg  16747  elcls  17125  isclo  17139  ptbasfi  17601  ptopn2  17604  xkopt  17675  kqdisj  17752  fin1aufil  17952  ptcmplem4  18074  opnsubg  18125  tsmssplit  18169  zcld  18832  recld2  18833  reconnlem1  18845  ioombl1lem4  19443  i1fima2sn  19560  itg1val2  19564  i1f0  19567  itg1addlem4  19579  mbfi1flim  19603  itg2splitlem  19628  itg2split  19629  itg2cnlem1  19641  itg2cnlem2  19642  itgss2  19692  itgeqa  19693  itgss3  19694  itgless  19696  ibladdlem  19699  itgaddlem1  19702  iblabslem  19707  itggt0  19721  itgcn  19722  evlslem3  19923  evlslem1  19924  ply1termlem  20110  plypf1  20119  plyaddlem1  20120  plymullem1  20121  coeeulem  20131  coeidlem  20144  coeid3  20147  coefv0  20154  coemulc  20161  dvply1  20189  vieta1lem2  20216  aaliou2  20245  logdmnrp  20520  chpub  20992  chebbnd1lem1  21151  strlem1  23741  partfun  24075  elzdif0  24352  indval2  24400  ind0  24405  sigaclfu2  24492  regamcl  24833  lgam1  24836  gam1  24837  facgam  24838  prodrblem  25244  fprodcvg  25245  prodmolem2a  25249  fprodss  25263  fprodsplit  25278  dfon2lem6  25399  wfrlem10  25520  wfrlem13  25523  wfrlem16  25526  ibladdnclem  26207  itgaddnclem1  26209  iblabsnclem  26214  dvreasin  26226  pridlc2  26619  pridlc3  26620  irrapx1  26828  pellqrex  26879  qirropth  26908  setindtr  27032  kelac1  27076  flcidc  27294  stoweidlem34  27697  stoweidlem44  27707  stirlinglem5  27741
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-dif 3315
  Copyright terms: Public domain W3C validator