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

Theorem eldifn 3620
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 3479 . 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 1762    \ cdif 3466
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-dif 3472
This theorem is referenced by:  elndif  3621  noel  3782  disjel  3866  tz7.7  4897  funiunfv  6139  tfi  6659  peano5  6694  tz7.48-2  7097  tz7.49  7100  oaf1o  7202  undifixp  7495  domdifsn  7590  isinf  7723  ordtypelem7  7938  unxpwdom2  8003  inf3lem3  8036  infdifsn  8062  cantnfp1lem1  8086  cantnfp1lem3  8088  cantnflem1d  8096  cantnfp1lem1OLD  8112  cantnfp1lem3OLD  8114  cantnflem1dOLD  8119  setind  8154  fin23lem30  8711  domtriomlem  8811  axdc3lem4  8822  axdc4lem  8824  axcclem  8826  ttukeylem7  8884  konigthlem  8932  fpwwe2lem13  9009  fpwwe2  9010  hashf1lem1  12457  rlimrecl  13352  sumrblem  13482  fsumcvg  13483  summolem2a  13486  fsumss  13496  sumss2  13497  binomlem  13593  isumltss  13612  prmreclem2  14283  prmreclem5  14286  ramub1lem1  14392  efgs1b  16543  gsumzsplit  16728  gsumzsplitOLD  16729  gsum2d  16783  gsum2dOLD  16784  gsum2d2lem  16785  dmdprdsplitlem  16867  dmdprdsplitlemOLD  16868  pgpfac1lem1  16908  irredrmul  17133  lbsextlem2  17581  lbsextlem4  17583  psrlidm  17820  psrlidmOLD  17821  mplcoe1  17891  mplcoe5  17895  mplcoe2OLD  17897  evlslem3  17947  evlslem1  17948  cnsubrg  18239  maducoeval2  18902  madugsum  18905  elcls  19333  isclo  19347  ptbasfi  19810  ptopn2  19813  xkopt  19884  kqdisj  19961  fin1aufil  20161  ptcmplem4  20283  opnsubg  20334  tsmssplit  20382  zcld  21046  recld2  21047  reconnlem1  21059  ioombl1lem4  21699  i1fima2sn  21815  itg1val2  21819  i1f0  21822  itg1addlem4  21834  mbfi1flim  21858  itg2splitlem  21883  itg2split  21884  itg2cnlem1  21896  itg2cnlem2  21897  itgss2  21947  itgeqa  21948  itgss3  21949  itgless  21951  ibladdlem  21954  itgaddlem1  21957  iblabslem  21962  itggt0  21976  itgcn  21977  ply1termlem  22328  plypf1  22337  plyaddlem1  22338  plymullem1  22339  coeeulem  22349  coeidlem  22362  coeid3  22365  coefv0  22372  coemulc  22379  dvply1  22407  vieta1lem2  22434  aaliou2  22463  logdmnrp  22743  chpub  23216  chebbnd1lem1  23375  strlem1  26831  partfun  27174  elzdif0  27583  indval2  27654  ind0  27659  sigaclfu2  27747  eulerpartlemb  27933  regamcl  28229  lgam1  28232  gam1  28233  facgam  28234  prodrblem  28624  fprodcvg  28625  prodmolem2a  28629  fprodss  28643  fprodsplit  28658  dfon2lem6  28783  wfrlem10  28915  wfrlem13  28918  wfrlem16  28921  ibladdnclem  29635  itgaddnclem1  29637  iblabsnclem  29642  ftc1anclem5  29658  ftc1anclem6  29659  ftc1anclem8  29661  dvasin  29667  dvacos  29668  pridlc2  30059  pridlc3  30060  irrapx1  30355  pellqrex  30406  qirropth  30435  setindtr  30559  kelac1  30602  flcidc  30717  arearect  30777  areaquad  30778  sumnnodd  31127  stoweidlem34  31289  stoweidlem44  31299  stirlinglem5  31333  dirkercncflem1  31358  fourierdlem62  31424  fouriersw  31487
  Copyright terms: Public domain W3C validator