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

Theorem n0i 3716
Description: If a set has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
n0i  |-  ( B  e.  A  ->  -.  A  =  (/) )

Proof of Theorem n0i
StepHypRef Expression
1 noel 3715 . . 3  |-  -.  B  e.  (/)
2 eleq2 2455 . . 3  |-  ( A  =  (/)  ->  ( B  e.  A  <->  B  e.  (/) ) )
31, 2mtbiri 301 . 2  |-  ( A  =  (/)  ->  -.  B  e.  A )
43con2i 120 1  |-  ( B  e.  A  ->  -.  A  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1399    e. wcel 1826   (/)c0 3711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-dif 3392  df-nul 3712
This theorem is referenced by:  ne0i  3717  oprcl  4156  disjss3  4366  iin0  4539  snsn0non  4910  mptrcl  5863  isomin  6134  ovrcl  6229  tfrlem16  6980  oalimcl  7127  omlimcl  7145  oaabs2  7212  ecexr  7234  elpmi  7356  elmapex  7358  pmresg  7365  pmsspw  7372  ixpssmap2g  7417  ixpssmapg  7418  resixpfo  7426  php3  7622  cantnfp1lem2  8011  cantnflem1  8021  cantnfp1lem2OLD  8037  cantnflem1OLD  8044  cnfcom2lem  8058  cnfcom2lemOLD  8066  rankxplim2  8211  rankxplim3  8212  cardlim  8266  alephnbtwn  8365  pwcdadom  8509  ttukeylem5  8806  r1wunlim  9026  nnunb  10708  ssnn0fi  11997  ruclem13  13977  ramtub  14532  elbasfv  14683  elbasov  14684  restsspw  14839  homarcl  15424  grpidval  16004  odlem2  16680  efgrelexlema  16884  subcmn  16962  dvdsrval  17407  pf1rcl  18498  elocv  18790  matrcl  18999  0top  19570  ppttop  19593  pptbas  19594  restrcl  19744  ssrest  19763  iscnp2  19826  lmmo  19967  zfbas  20482  rnelfmlem  20538  isfcls  20595  isnghm  21315  iscau2  21801  itg2cnlem1  22253  itgsubstlem  22534  dchrrcl  23632  eleenn  24320  nbgranself2  24557  uvtxisvtx  24611  uvtx01vtx  24613  2spot0  25185  hon0  26828  dmadjrnb  26941  eulerpartlemgvv  28498  indispcon  28868  cvmtop1  28894  cvmtop2  28895  mrsub0  29065  mrsubf  29066  mrsubccat  29067  mrsubcn  29068  mrsubco  29070  mrsubvrs  29071  msubf  29081  mclsrcl  29110  funpartlem  29745  tailfb  30361  mapco2g  30812  wepwsolem  31153  ssfiunibd  31675  bnj98  34272  atbase  35427  llnbase  35646  lplnbase  35671  lvolbase  35715  osumcllem4N  36096  pexmidlem1N  36107  lhpbase  36135
  Copyright terms: Public domain W3C validator