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

Theorem n0i 3473
Description: If a set has elements, 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 3472 . . 3  |-  -.  B  e.  (/)
2 eleq2 2357 . . 3  |-  ( A  =  (/)  ->  ( B  e.  A  <->  B  e.  (/) ) )
31, 2mtbiri 294 . 2  |-  ( A  =  (/)  ->  -.  B  e.  A )
43con2i 112 1  |-  ( B  e.  A  ->  -.  A  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1632    e. wcel 1696   (/)c0 3468
This theorem is referenced by:  ne0i  3474  oprcl  3836  disjss3  4038  iin0  4200  snsn0non  4527  isomin  5850  ovrcl  5904  tfrlem16  6425  oalimcl  6574  omlimcl  6592  oaabs2  6659  ecexr  6681  elpmi  6805  elmapex  6807  pmresg  6811  pmsspw  6818  ixpssmap2g  6861  ixpssmapg  6862  resixpfo  6870  php3  7063  cantnfp1lem2  7397  cantnflem1  7407  cnfcom2lem  7420  rankxplim2  7566  rankxplim3  7567  cardlim  7621  alephnbtwn  7714  pwcdadom  7858  ttukeylem5  8156  r1wunlim  8375  nnunb  9977  ruclem13  12536  ramtub  13075  elbasfv  13207  elbasov  13208  restsspw  13352  homarcl  13876  grpidval  14400  odlem2  14870  efgrelexlema  15074  subcmn  15149  dvdsrval  15443  psr1rclOLD  16295  ply1rclOLD  16298  elocv  16584  tgclb  16724  0top  16737  ppttop  16760  pptbas  16761  restrcl  16904  ssrest  16923  iscnp2  16985  lmmo  17124  zfbas  17607  rnelfmlem  17663  isfcls  17720  isnghm  18248  iscau2  18719  itg2cnlem1  19132  itgsubstlem  19411  pf1rcl  19448  dchrrcl  20495  hon0  22389  dmadjrnb  22502  indispcon  23780  cvmtop1  23806  cvmtop2  23807  funpartlem  24552  eleenn  24596  dffprod  25422  tailfb  26429  mapco2g  26893  wepwsolem  27241  matrcl  27569  nbgranself2  28285  uvtxisvtx  28303  uvtx01vtx  28305  bnj98  29215  atbase  30101  llnbase  30320  lplnbase  30345  lvolbase  30389  osumcllem4N  30770  pexmidlem1N  30781  lhpbase  30809
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-nul 3469
  Copyright terms: Public domain W3C validator