Theorem n0i 3727

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

Assertion

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

Proof of Theorem n0i

Step	Hyp	Ref	Expression
1		noel 3726	. . 3 |- -. B e. (/)
2		eleq2 2538	. . 3 |- ( A = (/) -> ( B e. A <-> B e. (/) ) )
3	1, 2	mtbiri 310	. 2 |- ( A = (/) -> -. B e. A )
4	3	con2i 124	1 |- ( B e. A -> -. A = (/) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1452   e. wcel 1904   (/)c0 3722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-dif 3393  df-nul 3723

This theorem is referenced by:  ne0i  3728  oprcl  4183  disjss3  4394  iin0  4575  snsn0non  5548  mptrcl  5970  isomin  6246  ovrcl  6341  tfrlem16  7129  oalimcl  7279  omlimcl  7297  oaabs2  7364  ecexr  7386  elpmi  7508  elmapex  7510  pmresg  7517  pmsspw  7524  ixpssmap2g  7569  ixpssmapg  7570  resixpfo  7578  php3  7776  cantnfp1lem2  8202  cantnflem1  8212  cnfcom2lem  8224  rankxplim2  8369  rankxplim3  8370  cardlim  8424  alephnbtwn  8520  pwcdadom  8664  ttukeylem5  8961  r1wunlim  9180  nnunb  10889  ssnn0fi  12235  ruclem13  14371  ramtub  15047  ramtubOLD  15048  elbasfv  15248  elbasov  15249  restsspw  15408  homarcl  16001  grpidval  16581  odlem2  17266  odlem2OLD  17282  efgrelexlema  17477  subcmn  17555  dvdsrval  17951  pf1rcl  19014  elocv  19308  matrcl  19514  0top  20076  ppttop  20099  pptbas  20100  restrcl  20250  ssrest  20269  iscnp2  20332  lmmo  20473  zfbas  20989  rnelfmlem  21045  isfcls  21102  isnghm  21806  isnghmOLD  21824  iscau2  22325  itg2cnlem1  22798  itgsubstlem  23079  dchrrcl  24247  eleenn  25005  nbgranself2  25243  uvtxisvtx  25297  uvtx01vtx  25299  2spot0  25871  hon0  27527  dmadjrnb  27640  eulerpartlemgvv  29282  bnj98  29750  indispcon  30029  cvmtop1  30055  cvmtop2  30056  mrsub0  30226  mrsubf  30227  mrsubccat  30228  mrsubcn  30229  mrsubco  30231  mrsubvrs  30232  msubf  30242  mclsrcl  30271  funpartlem  30780  tailfb  31104  atbase  32926  llnbase  33145  lplnbase  33170  lvolbase  33214  osumcllem4N  33595  pexmidlem1N  33606  lhpbase  33634  mapco2g  35627  wepwsolem  35971  ssfiunibd  37615  hoicvr  38488