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

Theorem n0i 3635
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 3634 . . 3  |-  -.  B  e.  (/)
2 eleq2 2499 . . 3  |-  ( A  =  (/)  ->  ( B  e.  A  <->  B  e.  (/) ) )
31, 2mtbiri 296 . 2  |-  ( A  =  (/)  ->  -.  B  e.  A )
43con2i 115 1  |-  ( B  e.  A  ->  -.  A  =  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1653    e. wcel 1726   (/)c0 3630
This theorem is referenced by:  ne0i  3636  oprcl  4010  disjss3  4213  iin0  4375  snsn0non  4702  isomin  6059  ovrcl  6113  tfrlem16  6656  oalimcl  6805  omlimcl  6823  oaabs2  6890  ecexr  6912  elpmi  7037  elmapex  7039  pmresg  7043  pmsspw  7050  ixpssmap2g  7093  ixpssmapg  7094  resixpfo  7102  php3  7295  cantnfp1lem2  7637  cantnflem1  7647  cnfcom2lem  7660  rankxplim2  7806  rankxplim3  7807  cardlim  7861  alephnbtwn  7954  pwcdadom  8098  ttukeylem5  8395  r1wunlim  8614  nnunb  10219  ruclem13  12843  ramtub  13382  elbasfv  13514  elbasov  13515  restsspw  13661  homarcl  14185  grpidval  14709  odlem2  15179  efgrelexlema  15383  subcmn  15458  dvdsrval  15752  elocv  16897  0top  17050  ppttop  17073  pptbas  17074  restrcl  17223  ssrest  17242  iscnp2  17305  lmmo  17446  zfbas  17930  rnelfmlem  17986  isfcls  18043  isnghm  18759  iscau2  19232  itg2cnlem1  19655  itgsubstlem  19934  pf1rcl  19971  dchrrcl  21026  nbgranself2  21450  uvtxisvtx  21501  uvtx01vtx  21503  hon0  23298  dmadjrnb  23411  indispcon  24923  cvmtop1  24949  cvmtop2  24950  funpartlem  25789  eleenn  25837  tailfb  26408  mapco2g  26771  wepwsolem  27118  matrcl  27445  2spot0  28515  bnj98  29300  atbase  30149  llnbase  30368  lplnbase  30393  lvolbase  30437  osumcllem4N  30818  pexmidlem1N  30829  lhpbase  30857
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-dif 3325  df-nul 3631
  Copyright terms: Public domain W3C validator