ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ne0i GIF version

Theorem ne0i 3339
Description: If a set has elements, it is not empty. A set with elements is also inhabited, see elex2 2676. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
ne0i (𝐵𝐴𝐴 ≠ ∅)

Proof of Theorem ne0i
StepHypRef Expression
1 n0i 3338 . 2 (𝐵𝐴 → ¬ 𝐴 = ∅)
21neneqad 2364 1 (𝐵𝐴𝐴 ≠ ∅)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1465  wne 2285  c0 3333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ne 2286  df-v 2662  df-dif 3043  df-nul 3334
This theorem is referenced by:  ne0d  3340  ne0ii  3342  vn0  3343  inelcm  3393  rzal  3430  rexn0  3431  snnzg  3610  prnz  3615  tpnz  3618  brne0  3947  onn0  4292  nn0eln0  4503  ordge1n0im  6301  nnmord  6381  map0g  6550  phpm  6727  fiintim  6785  addclpi  7103  mulclpi  7104  uzn0  9309  iccsupr  9717
  Copyright terms: Public domain W3C validator