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

Theorem eldifn 3299
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 3162 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simprbi 450 1  |-  ( A  e.  ( B  \  C )  ->  -.  A  e.  C )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1684    \ cdif 3149
This theorem is referenced by:  elndif  3300  noel  3459  disjel  3501  tz7.7  4418  tfi  4644  peano5  4679  funiunfv  5774  tz7.48-2  6454  tz7.49  6457  oaf1o  6561  undifixp  6852  boxcutc  6859  domdifsn  6945  isinf  7076  ordtypelem7  7239  unxpwdom2  7302  inf3lem3  7331  infdifsn  7357  cantnfp1lem1  7380  cantnfp1lem3  7382  cantnflem1d  7390  cantnflem2  7392  setind  7419  ackbij1lem18  7863  infpssrlem4  7932  fin23lem30  7968  domtriomlem  8068  axdc3lem4  8079  axdc4lem  8081  axcclem  8083  ttukeylem7  8142  konigthlem  8190  fpwwe2lem13  8264  fpwwe2  8265  pwfseqlem4  8284  hashf1lem1  11393  rlimrecl  12054  sumrblem  12184  fsumcvg  12185  summolem2a  12188  fsumss  12198  sumss2  12199  binomlem  12287  isumltss  12307  rpnnen2lem9  12501  prmreclem2  12964  prmreclem5  12967  ramub1lem1  13073  ramub1lem2  13074  efgs1b  15045  gsumzsplit  15206  gsum2d  15223  gsum2d2lem  15224  dprdfadd  15255  dmdprdsplitlem  15272  pgpfac1lem1  15309  pgpfac1lem2  15310  pgpfac1lem3a  15311  pgpfac1lem3  15312  irredrmul  15489  lspsolv  15896  lsppratlem3  15902  islbs3  15908  lbsextlem2  15912  lbsextlem4  15914  psrlidm  16148  mplsubrglem  16183  mplcoe1  16209  mplcoe2  16211  cnsubrg  16432  elcls  16810  isclo  16824  hauscmplem  17133  1stccnp  17188  1stckgen  17249  ptbasfi  17276  ptopn2  17279  xkopt  17349  kqdisj  17423  ufinffr  17624  fin1aufil  17627  alexsublem  17738  ptcmplem4  17749  opnsubg  17790  tsmssplit  17834  zcld  18319  recld2  18320  reconnlem1  18331  bcthlem4  18749  ioombl1lem4  18918  i1fima2sn  19035  i1fd  19036  itg1val2  19039  i1f0  19042  itg1addlem4  19054  mbfi1flim  19078  itg2splitlem  19103  itg2split  19104  itg2cnlem1  19116  itg2cnlem2  19117  itgss2  19167  itgeqa  19168  itgss3  19169  itgless  19171  ibladdlem  19174  itgaddlem1  19177  iblabslem  19182  itggt0  19196  itgcn  19197  evlslem3  19398  evlslem1  19399  ply1termlem  19585  plyeq0lem  19592  plypf1  19594  plyaddlem1  19595  plymullem1  19596  coeeulem  19606  coeidlem  19619  coeid3  19622  coefv0  19629  coemulc  19636  dvply1  19664  vieta1lem2  19691  aaliou2  19720  logdmnrp  19988  chpub  20459  chebbnd1lem1  20618  strlem1  22830  partfun  23240  sigaclfu2  23482  indval2  23598  ind0  23603  dfon2lem6  24144  wfrlem10  24265  wfrlem13  24268  wfrlem16  24271  onint1  24888  dvreasin  24923  bsstr  26128  nbssntr  26129  lppotos  26144  bsstrs  26146  nbssntrs  26147  bosser  26167  pdiveql  26168  pridlc2  26697  pridlc3  26698  irrapx1  26913  pellqrex  26964  rmspecnonsq  26992  qirropth  26993  setindtr  27117  kelac1  27161  frlmssuvc2  27247  flcidc  27379  stoweidlem34  27783  stoweidlem43  27792  stoweidlem44  27793  stirlinglem5  27827  dochnel2  31582
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155
  Copyright terms: Public domain W3C validator