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

Theorem n0i 3460
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 3459 . . 3  |-  -.  B  e.  (/)
2 eleq2 2344 . . 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 1623    e. wcel 1684   (/)c0 3455
This theorem is referenced by:  ne0i  3461  oprcl  3820  disjss3  4022  iin0  4184  snsn0non  4511  isomin  5834  ovrcl  5888  tfrlem16  6409  oalimcl  6558  omlimcl  6576  oaabs2  6643  ecexr  6665  elpmi  6789  elmapex  6791  pmresg  6795  pmsspw  6802  ixpssmap2g  6845  ixpssmapg  6846  resixpfo  6854  php3  7047  cantnfp1lem2  7381  cantnflem1  7391  cnfcom2lem  7404  rankxplim2  7550  rankxplim3  7551  cardlim  7605  alephnbtwn  7698  pwcdadom  7842  ttukeylem5  8140  r1wunlim  8359  nnunb  9961  ruclem13  12520  ramtub  13059  elbasfv  13191  elbasov  13192  restsspw  13336  homarcl  13860  grpidval  14384  odlem2  14854  efgrelexlema  15058  subcmn  15133  dvdsrval  15427  psr1rclOLD  16279  ply1rclOLD  16282  elocv  16568  tgclb  16708  0top  16721  ppttop  16744  pptbas  16745  restrcl  16888  ssrest  16907  iscnp2  16969  lmmo  17108  zfbas  17591  rnelfmlem  17647  isfcls  17704  isnghm  18232  iscau2  18703  itg2cnlem1  19116  itgsubstlem  19395  pf1rcl  19432  dchrrcl  20479  hon0  22373  dmadjrnb  22486  indispcon  23765  cvmtop1  23791  cvmtop2  23792  eleenn  24524  dffprod  25319  tailfb  26326  mapco2g  26790  wepwsolem  27138  matrcl  27466  nbgranself2  28151  uvtxisvtx  28162  uvtx01vtx  28164  bnj98  28899  atbase  29479  llnbase  29698  lplnbase  29723  lvolbase  29767  osumcllem4N  30148  pexmidlem1N  30159  lhpbase  30187
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-nul 3456
  Copyright terms: Public domain W3C validator