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

Theorem eldifn 3301
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 3164 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simprbi 452 1  |-  ( A  e.  ( B  \  C )  ->  -.  A  e.  C )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    e. wcel 1685    \ cdif 3151
This theorem is referenced by:  elndif  3302  noel  3461  disjel  3503  tz7.7  4418  tfi  4644  peano5  4679  funiunfv  5736  tz7.48-2  6450  tz7.49  6453  oaf1o  6557  undifixp  6848  boxcutc  6855  domdifsn  6941  isinf  7072  ordtypelem7  7235  unxpwdom2  7298  inf3lem3  7327  infdifsn  7353  cantnfp1lem1  7376  cantnfp1lem3  7378  cantnflem1d  7386  cantnflem2  7388  setind  7415  ackbij1lem18  7859  infpssrlem4  7928  fin23lem30  7964  domtriomlem  8064  axdc3lem4  8075  axdc4lem  8077  axcclem  8079  ttukeylem7  8138  konigthlem  8186  fpwwe2lem13  8260  fpwwe2  8261  pwfseqlem4  8280  hashf1lem1  11388  rlimrecl  12049  sumrblem  12179  fsumcvg  12180  summolem2a  12183  fsumss  12193  sumss2  12194  binomlem  12282  isumltss  12302  rpnnen2lem9  12496  prmreclem2  12959  prmreclem5  12962  ramub1lem1  13068  ramub1lem2  13069  efgs1b  15040  gsumzsplit  15201  gsum2d  15218  gsum2d2lem  15219  dprdfadd  15250  dmdprdsplitlem  15267  pgpfac1lem1  15304  pgpfac1lem2  15305  pgpfac1lem3a  15306  pgpfac1lem3  15307  irredrmul  15484  lspsolv  15891  lsppratlem3  15897  islbs3  15903  lbsextlem2  15907  lbsextlem4  15909  psrlidm  16143  mplsubrglem  16178  mplcoe1  16204  mplcoe2  16206  cnsubrg  16427  elcls  16805  isclo  16819  hauscmplem  17128  1stccnp  17183  1stckgen  17244  ptbasfi  17271  ptopn2  17274  xkopt  17344  kqdisj  17418  ufinffr  17619  fin1aufil  17622  alexsublem  17733  ptcmplem4  17744  opnsubg  17785  tsmssplit  17829  zcld  18314  recld2  18315  reconnlem1  18326  bcthlem4  18744  ioombl1lem4  18913  i1fima2sn  19030  i1fd  19031  itg1val2  19034  i1f0  19037  itg1addlem4  19049  mbfi1flim  19073  itg2splitlem  19098  itg2split  19099  itg2cnlem1  19111  itg2cnlem2  19112  itgss2  19162  itgeqa  19163  itgss3  19164  itgless  19166  ibladdlem  19169  itgaddlem1  19172  iblabslem  19177  itggt0  19191  itgcn  19192  evlslem3  19393  evlslem1  19394  ply1termlem  19580  plyeq0lem  19587  plypf1  19589  plyaddlem1  19590  plymullem1  19591  coeeulem  19601  coeidlem  19614  coeid3  19617  coefv0  19624  coemulc  19631  dvply1  19659  vieta1lem2  19686  aaliou2  19715  logdmnrp  19983  chpub  20454  chebbnd1lem1  20613  strlem1  22823  dfon2lem6  23546  wfrlem10  23667  wfrlem13  23670  wfrlem16  23673  onint1  24296  bsstr  25528  nbssntr  25529  lppotos  25544  bsstrs  25546  nbssntrs  25547  bosser  25567  pdiveql  25568  pridlc2  26097  pridlc3  26098  irrapx1  26313  pellqrex  26364  rmspecnonsq  26392  qirropth  26393  setindtr  26517  kelac1  26561  frlmssuvc2  26647  flcidc  26779  stoweidlem34  27183  stoweidlem43  27192  stoweidlem44  27193  stirlinglem5  27227  dochnel2  30850
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-dif 3157
  Copyright terms: Public domain W3C validator