Theorem ne0i 3364

Description: If a set has elements, it is not empty. A set with elements is also inhabited, see elex2 2697. (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
ne0i	|- ( B e. A -> A =/= (/) )

Proof of Theorem ne0i

Step	Hyp	Ref	Expression
1		n0i 3363	. 2 |- ( B e. A -> -. A = (/) )
2	1	neneqad 2385	1 |- ( B e. A -> A =/= (/) )

Syntax hints:   -> wi 4   e. wcel 1480   =/= wne 2306   (/)c0 3358

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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ne 2307  df-v 2683  df-dif 3068  df-nul 3359

This theorem is referenced by:  ne0d  3365  ne0ii  3367  vn0  3368  inelcm  3418  rzal  3455  rexn0  3456  snnzg  3635  prnz  3640  tpnz  3643  brne0  3972  onn0  4317  nn0eln0  4528  ordge1n0im  6326  nnmord  6406  map0g  6575  phpm  6752  fiintim  6810  addclpi  7128  mulclpi  7129  uzn0  9334  iccsupr  9742