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

Theorem eldifn 3568
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 3426 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simprbi 470 1  |-  ( A  e.  ( B  \  C )  ->  -.  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1898    \ cdif 3413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-dif 3419
This theorem is referenced by:  elndif  3569  noel  3747  disjel  3823  tz7.7  5468  funiunfv  6178  tfi  6707  peano5  6743  wfrlem10  7071  wfrlem13  7074  wfrlem16  7077  tz7.48-2  7185  tz7.49  7188  oaf1o  7290  undifixp  7584  domdifsn  7681  isinf  7811  ordtypelem7  8065  unxpwdom2  8129  inf3lem3  8161  infdifsn  8188  cantnfp1lem1  8209  cantnfp1lem3  8211  cantnflem1d  8219  setind  8244  fin23lem30  8798  domtriomlem  8898  axdc3lem4  8909  axdc4lem  8911  axcclem  8913  ttukeylem7  8971  konigthlem  9019  fpwwe2lem13  9093  fpwwe2  9094  hashf1lem1  12651  rlimrecl  13693  sumrblem  13826  fsumcvg  13827  summolem2a  13830  fsumss  13840  sumss2  13841  binomlem  13936  isumltss  13955  prodrblem  14032  fprodcvg  14033  prodmolem2a  14037  fprodss  14051  fprodsplit  14069  prmreclem2  14910  prmreclem5  14913  ramub1lem1  15033  efgs1b  17435  gsumzsplit  17609  gsum2d  17653  gsum2d2lem  17654  dmdprdsplitlem  17719  pgpfac1lem1  17756  irredrmul  17984  lbsextlem2  18431  lbsextlem4  18433  psrlidm  18676  mplcoe1  18738  mplcoe5  18741  evlslem3  18786  evlslem1  18787  cnsubrg  19077  maducoeval2  19714  madugsum  19717  elcls  20138  isclo  20152  ptbasfi  20645  ptopn2  20648  xkopt  20719  kqdisj  20796  fin1aufil  20996  ptcmplem4  21119  opnsubg  21171  tsmssplit  21215  zcld  21880  recld2  21881  reconnlem1  21893  ioombl1lem4  22563  i1fima2sn  22687  itg1val2  22691  i1f0  22694  itg1addlem4  22706  mbfi1flim  22730  itg2splitlem  22755  itg2split  22756  itg2cnlem1  22768  itg2cnlem2  22769  itgss2  22819  itgeqa  22820  itgss3  22821  itgless  22823  ibladdlem  22826  itgaddlem1  22829  iblabslem  22834  itggt0  22848  itgcn  22849  ply1termlem  23206  plypf1  23215  plyaddlem1  23216  plymullem1  23217  coeeulem  23227  coeidlem  23240  coeid3  23243  coefv0  23251  coemulc  23258  dvply1  23286  vieta1lem2  23313  aaliou2  23345  logdmnrp  23635  regamcl  24035  lgam1  24038  gam1  24039  facgam  24040  chpub  24197  chebbnd1lem1  24356  strlem1  27952  partfun  28327  elzdif0  28833  indval2  28885  ind0  28890  sigaclfu2  28992  eulerpartlemb  29250  mrsubcn  30206  dfon2lem6  30483  ibladdnclem  32043  itgaddnclem1  32045  iblabsnclem  32050  ftc1anclem5  32066  ftc1anclem6  32067  ftc1anclem8  32069  dvasin  32073  dvacos  32074  pridlc2  32350  pridlc3  32351  irrapx1  35717  pellqrex  35771  qirropth  35801  setindtr  35924  kelac1  35966  flcidc  36085  arearect  36145  areaquad  36146  mpct  37520  iccdificc  37679  fsumsupp0  37695  mccllem  37715  sumnnodd  37748  fprodcncf  37817  stoweidlem34  37933  stoweidlem44  37943  stirlinglem5  37978  fourierdlem62  38070  fouriersw  38133  elaa2lem  38135  elaa2lemOLD  38136  etransclem44  38181  sge0iunmptlemfi  38293  sge0fodjrnlem  38296  iundjiunlem  38335  meadjiunlem  38341  isomenndlem  38389  hsphoidmvle2  38445  hsphoidmvle  38446  hspdifhsp  38476  hspmbllem2  38487
  Copyright terms: Public domain W3C validator