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

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

Proof of Theorem ne0i
StepHypRef Expression
1 n0i 3307 . 2 (𝐵𝐴 → ¬ 𝐴 = ∅)
21neneqad 2341 1 (𝐵𝐴𝐴 ≠ ∅)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1445  wne 2262  c0 3302
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-v 2635  df-dif 3015  df-nul 3303
This theorem is referenced by:  ne0d  3309  ne0ii  3311  vn0  3312  inelcm  3362  rzal  3399  rexn0  3400  snnzg  3579  prnz  3584  tpnz  3587  onn0  4251  nn0eln0  4461  ordge1n0im  6238  nnmord  6316  map0g  6485  phpm  6661  fiintim  6719  addclpi  6983  mulclpi  6984  uzn0  9133  iccsupr  9532
  Copyright terms: Public domain W3C validator