Theorem n0i 2275

Description: If a set has elements, it is not empty.

Assertion

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

Proof of Theorem n0i

Step	Hyp	Ref	Expression
1		noel 2274	. . 3 |- -. B e. (/)
2		eleq2 1527	. . 3 |- (A = (/) -> (B e. A <-> B e. (/)))
3	1, 2	mtbiri 715	. 2 |- (A = (/) -> -. B e. A)
4	3	con2i 97	1 |- (B e. A -> -. A = (/))

Syntax hints:  -. wn 2   -> wi 3   = wceq 953   e. wcel 955  (/)c0 2270

This theorem is referenced by:  ne0i 2276  iununi 2606  iin0 2730  opnz 2785  frirr 2914  funiunfv 3851  isomin 3884  oalimcl 4178  omlimcl 4193  ixp0 4345  php3 4495  r1pwcl 4659  rankxplim2 4685  rankxplim3 4686  cardlim 4823  alephnbtwn 4840  suppsrlem 5193  suprelem 5231  nnunb 6017  elfzlem 6405  fznt 6425  sqrlem6 6608  0top 7577  issubg 8053  hon0 9636  dmadjrnb 9747

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-dif 2039  df-nul 2271

Copyright terms: Public domain