Theorem n0i 3630

Description: If a set has elements, 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 3629	. . 3 |- -. B e. (/)
2		eleq2 2494	. . 3 |- ( A = (/) -> ( B e. A <-> B e. (/) ) )
3	1, 2	mtbiri 303	. 2 |- ( A = (/) -> -. B e. A )
4	3	con2i 120	1 |- ( B e. A -> -. A = (/) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1362   e. wcel 1755   (/)c0 3625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-dif 3319  df-nul 3626

This theorem is referenced by:  ne0i  3631  oprcl  4072  disjss3  4279  iin0  4454  snsn0non  4824  isomin  6015  ovrcl  6110  tfrlem16  6838  oalimcl  6987  omlimcl  7005  oaabs2  7072  ecexr  7094  elpmi  7219  elmapex  7221  pmresg  7228  pmsspw  7235  ixpssmap2g  7280  ixpssmapg  7281  resixpfo  7289  php3  7485  cantnfp1lem2  7875  cantnflem1  7885  cantnfp1lem2OLD  7901  cantnflem1OLD  7908  cnfcom2lem  7922  cnfcom2lemOLD  7930  rankxplim2  8075  rankxplim3  8076  cardlim  8130  alephnbtwn  8229  pwcdadom  8373  ttukeylem5  8670  r1wunlim  8892  nnunb  10563  ruclem13  13507  ramtub  14056  elbasfv  14204  elbasov  14205  restsspw  14353  homarcl  14879  grpidval  15415  odlem2  16022  efgrelexlema  16226  subcmn  16301  dvdsrval  16671  elocv  17935  matrcl  18154  0top  18430  ppttop  18453  pptbas  18454  restrcl  18603  ssrest  18622  iscnp2  18685  lmmo  18826  zfbas  19311  rnelfmlem  19367  isfcls  19424  isnghm  20144  iscau2  20630  itg2cnlem1  21081  itgsubstlem  21362  pf1rcl  21400  dchrrcl  22464  eleenn  22965  nbgranself2  23170  uvtxisvtx  23221  uvtx01vtx  23223  hon0  25020  dmadjrnb  25133  eulerpartlemgvv  26607  indispcon  26971  cvmtop1  26997  cvmtop2  26998  funpartlem  27820  tailfb  28442  mapco2g  28895  wepwsolem  29239  2spot0  30503  bnj98  31562  atbase  32507  llnbase  32726  lplnbase  32751  lvolbase  32795  osumcllem4N  33176  pexmidlem1N  33187  lhpbase  33215