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

Theorem eldifn 3531
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 3389 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simprbi 465 1  |-  ( A  e.  ( B  \  C )  ->  -.  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1872    \ cdif 3376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-dif 3382
This theorem is referenced by:  elndif  3532  noel  3708  disjel  3784  tz7.7  5411  funiunfv  6112  tfi  6638  peano5  6674  wfrlem10  7000  wfrlem13  7003  wfrlem16  7006  tz7.48-2  7114  tz7.49  7117  oaf1o  7219  undifixp  7513  domdifsn  7608  isinf  7738  ordtypelem7  7992  unxpwdom2  8056  inf3lem3  8088  infdifsn  8114  cantnfp1lem1  8135  cantnfp1lem3  8137  cantnflem1d  8145  setind  8170  fin23lem30  8723  domtriomlem  8823  axdc3lem4  8834  axdc4lem  8836  axcclem  8838  ttukeylem7  8896  konigthlem  8944  fpwwe2lem13  9018  fpwwe2  9019  hashf1lem1  12566  rlimrecl  13587  sumrblem  13720  fsumcvg  13721  summolem2a  13724  fsumss  13734  sumss2  13735  binomlem  13830  isumltss  13849  prodrblem  13926  fprodcvg  13927  prodmolem2a  13931  fprodss  13945  fprodsplit  13963  prmreclem2  14804  prmreclem5  14807  ramub1lem1  14927  efgs1b  17329  gsumzsplit  17503  gsum2d  17547  gsum2d2lem  17548  dmdprdsplitlem  17613  pgpfac1lem1  17650  irredrmul  17878  lbsextlem2  18325  lbsextlem4  18327  psrlidm  18570  mplcoe1  18632  mplcoe5  18635  evlslem3  18680  evlslem1  18681  cnsubrg  18971  maducoeval2  19607  madugsum  19610  elcls  20031  isclo  20045  ptbasfi  20538  ptopn2  20541  xkopt  20612  kqdisj  20689  fin1aufil  20889  ptcmplem4  21012  opnsubg  21064  tsmssplit  21108  zcld  21773  recld2  21774  reconnlem1  21786  ioombl1lem4  22456  i1fima2sn  22580  itg1val2  22584  i1f0  22587  itg1addlem4  22599  mbfi1flim  22623  itg2splitlem  22648  itg2split  22649  itg2cnlem1  22661  itg2cnlem2  22662  itgss2  22712  itgeqa  22713  itgss3  22714  itgless  22716  ibladdlem  22719  itgaddlem1  22722  iblabslem  22727  itggt0  22741  itgcn  22742  ply1termlem  23099  plypf1  23108  plyaddlem1  23109  plymullem1  23110  coeeulem  23120  coeidlem  23133  coeid3  23136  coefv0  23144  coemulc  23151  dvply1  23179  vieta1lem2  23206  aaliou2  23238  logdmnrp  23528  regamcl  23928  lgam1  23931  gam1  23932  facgam  23933  chpub  24090  chebbnd1lem1  24249  strlem1  27845  partfun  28224  elzdif0  28736  indval2  28788  ind0  28793  sigaclfu2  28895  eulerpartlemb  29153  mrsubcn  30109  dfon2lem6  30385  ibladdnclem  31905  itgaddnclem1  31907  iblabsnclem  31912  ftc1anclem5  31928  ftc1anclem6  31929  ftc1anclem8  31931  dvasin  31935  dvacos  31936  pridlc2  32212  pridlc3  32213  irrapx1  35585  pellqrex  35639  qirropth  35669  setindtr  35792  kelac1  35834  flcidc  35953  arearect  36013  areaquad  36014  mccllem  37560  sumnnodd  37593  fprodcncf  37662  stoweidlem34  37778  stoweidlem44  37788  stirlinglem5  37823  fourierdlem62  37915  fouriersw  37978  elaa2lem  37980  elaa2lemOLD  37981  etransclem44  38026  sge0iunmptlemfi  38106  sge0fodjrnlem  38109  iundjiunlem  38148  meadjiunlem  38154  isomenndlem  38202  hsphoidmvle2  38254  hsphoidmvle  38255
  Copyright terms: Public domain W3C validator