Theorem n0i 2288

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 2287	. . 3 |- -. B e. (/)
2		eleq2 1538	. . 3 |- (A = (/) -> (B e. A <-> B e. (/)))
3	1, 2	mtbiri 719	. 2 |- (A = (/) -> -. B e. A)
4	3	con2i 97	1 |- (B e. A -> -. A = (/))

Syntax hints:  -. wn 2   -> wi 3   = wceq 958   e. wcel 960  (/)c0 2283

This theorem is referenced by:  ne0i 2289  iununi 2621  iin0 2745  opnz 2801  frirr 2930  funiunfv 3872  isomin 3905  oalimcl 4200  omlimcl 4215  ixp0 4367  php3 4521  php3OLD 4522  r1pwcl 4697  rankxplim2 4723  rankxplim3 4724  cardlim 4862  alephnbtwn 4879  suppsrlem 5233  suprelem 5271  nnunb 6072  elfzlem 6474  fznt 6494  sqrlem6 6679  infpss 7575  0top 7634  issubg 8112  hon0 9714  dmadjrnb 9825

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-dif 2052  df-nul 2284

Copyright terms: Public domain