Theorem ne0i 3556

Description: If a set has elements, it is not empty. (Contributed by NM, 31-Dec-1993.)

Assertion

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

Proof of Theorem ne0i

Step	Hyp	Ref	Expression
1		n0i 3555	. 2 |- (B e. A -> -. A = (/))
2		df-ne 2518	. 2 |- (A =/= (/) <-> -. A = (/))
3	1, 2	sylibr 203	1 |- (B e. A -> A =/= (/))

Syntax hints:  -. wn 3   -> wi 4   = wceq 1642   e. 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