Theorem ne0i 3230

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

Assertion

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

Proof of Theorem ne0i

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

Syntax hints:   -> wi 4   e. wcel 1393   =/= wne 2204   (/)c0 3224

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-v 2559  df-dif 2920  df-nul 3225

This theorem is referenced by:  vn0  3231  inelcm  3282  rzal  3318  rexn0  3319  snnzg  3485  prnz  3490  tpnz  3493  onn0  4137  nn0eln0  4341  ordge1n0im  6019  nnmord  6090  phpm  6327  addclpi  6425  mulclpi  6426  uzn0  8488  iccsupr  8835