Theorem n0i 1712

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 1711	. . 3 |- -. B e. (/)
2		eleq2 1150	. . 3 |- (A = (/) -> (B e. A <-> B e. (/)))
3	1, 2	mtbiri 539	. 2 |- (A = (/) -> -. B e. A)
4	3	con2i 89	1 |- (B e. A -> -. A = (/))

Syntax hints:  -. wn 1   -> wi 2   = wceq 1091   e. wcel 1092  (/)c0 1707

This theorem is referenced by:  inelcm 1742  snnz 1846  prnz 1847  tpnz 1848  exss 1881  opnz 1897  iununi 2037  frirr 2176  onnmin 2270  ord0eln0 2278  onne0 2287  isomin 2937  isofrlem 2939  f1oweOLD 2944  oe1m 3147  oawordeulem 3156  oa00 3161  oalimcl 3162  nnmord 3189  php3 3411  unblem1 3431  inf1 3458  zfregs 3491  r1pwcl 3530  aceq5lem2 3559  kmlem6 3585  cardlim 3657  alephnbtwn 3674  addclpi 3814  mulclpi 3815  indpi 3828  1pr 3911  suppsrlem 4015  suprelem 4053  nnunb 4520  sqrlem6 4736  ruclem33 4917  projlem8 5200  shintclt 5295  chintclt 5297  hsupval2t 5301

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-nul 1708

metamath.org