NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ne0i Unicode version

Theorem ne0i 3556
Description: If a set has elements, it is not empty. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
ne0i

Proof of Theorem ne0i
StepHypRef Expression
1 n0i 3555 . 2
2 df-ne 2518 . 2
31, 2sylibr 203 1
Colors of variables: wff setvar class
Syntax hints:   wn 3   wi 4   wceq 1642   wcel 1710   wne 2516  c0 3550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-dif 3215  df-nul 3551
This theorem is referenced by:  vn0  3557  inelcm  3605  rzal  3651  rexn0  3652  snnzg  3833  prnz  3835  tpnz  3837  pw10b  4166  tfinnnul  4490  tfinpw1  4494  tfin1c  4499  0ceven  4505  sfintfin  4532  tfinnn  4534  sfinltfin  4535  sfin111  4536  vfinspnn  4541  vfin1cltv  4547  vfinncvntnn  4548  vinf  4555  nulnnn  4556  xpnz  5045  elfvdm  5351  elovex12  5648  map0  6025  xpsnen  6049  ncssfin  6151  ce0nnulb  6182
  Copyright terms: Public domain W3C validator