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

Theorem eldifn 3386
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 3248 . 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 1715    \ cdif 3235
This theorem is referenced by:  elndif  3387  noel  3547  disjel  3589  tz7.7  4521  tfi  4747  peano5  4782  funiunfv  5895  tz7.48-2  6596  tz7.49  6599  oaf1o  6703  undifixp  6995  boxcutc  7002  domdifsn  7088  isinf  7219  ordtypelem7  7386  unxpwdom2  7449  inf3lem3  7478  infdifsn  7504  cantnfp1lem1  7527  cantnfp1lem3  7529  cantnflem1d  7537  cantnflem2  7539  setind  7566  ackbij1lem18  8010  infpssrlem4  8079  fin23lem30  8115  domtriomlem  8215  axdc3lem4  8226  axdc4lem  8228  axcclem  8230  ttukeylem7  8289  konigthlem  8337  fpwwe2lem13  8411  fpwwe2  8412  pwfseqlem4  8431  hashf1lem1  11591  rlimrecl  12261  sumrblem  12392  fsumcvg  12393  summolem2a  12396  fsumss  12406  sumss2  12407  binomlem  12495  isumltss  12515  rpnnen2lem9  12709  prmreclem2  13172  prmreclem5  13175  ramub1lem1  13281  ramub1lem2  13282  efgs1b  15255  gsumzsplit  15416  gsum2d  15433  gsum2d2lem  15434  dprdfadd  15465  dmdprdsplitlem  15482  pgpfac1lem1  15519  pgpfac1lem2  15520  pgpfac1lem3a  15521  pgpfac1lem3  15522  irredrmul  15699  lspsolv  16106  lsppratlem3  16112  islbs3  16118  lbsextlem2  16122  lbsextlem4  16124  psrlidm  16358  mplsubrglem  16393  mplcoe1  16419  mplcoe2  16421  cnsubrg  16649  elcls  17027  isclo  17041  hauscmplem  17350  1stccnp  17405  1stckgen  17466  ptbasfi  17493  ptopn2  17496  xkopt  17566  kqdisj  17640  ufinffr  17837  fin1aufil  17840  alexsublem  17951  ptcmplem4  17962  opnsubg  18003  tsmssplit  18047  zcld  18532  recld2  18533  reconnlem1  18545  bcthlem4  18964  ioombl1lem4  19133  i1fima2sn  19250  i1fd  19251  itg1val2  19254  i1f0  19257  itg1addlem4  19269  mbfi1flim  19293  itg2splitlem  19318  itg2split  19319  itg2cnlem1  19331  itg2cnlem2  19332  itgss2  19382  itgeqa  19383  itgss3  19384  itgless  19386  ibladdlem  19389  itgaddlem1  19392  iblabslem  19397  itggt0  19411  itgcn  19412  evlslem3  19613  evlslem1  19614  ply1termlem  19800  plyeq0lem  19807  plypf1  19809  plyaddlem1  19810  plymullem1  19811  coeeulem  19821  coeidlem  19834  coeid3  19837  coefv0  19844  coemulc  19851  dvply1  19879  vieta1lem2  19906  aaliou2  19935  logdmnrp  20210  chpub  20682  chebbnd1lem1  20841  strlem1  23143  partfun  23490  indval2  23877  ind0  23882  sigaclfu2  23969  regamcl  24293  lgam1  24296  gam1  24297  facgam  24298  prodrblem  24739  fprodcvg  24740  prodmolem2a  24744  fprodss  24758  fprodsplit  24773  dfon2lem6  24885  wfrlem10  25006  wfrlem13  25009  wfrlem16  25012  onint1  25630  ibladdnclem  25679  itgaddnclem1  25681  iblabsnclem  25686  dvreasin  25698  pridlc2  26203  pridlc3  26204  irrapx1  26419  pellqrex  26470  rmspecnonsq  26498  qirropth  26499  setindtr  26623  kelac1  26667  frlmssuvc2  26753  flcidc  26885  stoweidlem34  27289  stoweidlem43  27298  stoweidlem44  27299  stirlinglem5  27333  dochnel2  31653
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-dif 3241
  Copyright terms: Public domain W3C validator