Theorem ne0i 2289

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

Assertion

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

Proof of Theorem ne0i

Step	Hyp	Ref	Expression
1		n0i 2288	. 2 |- (B e. A -> -. A = (/))
2		df-ne 1590	. 2 |- (A =/= (/) <-> -. A = (/))
3	1, 2	sylibr 200	1 |- (B e. A -> A =/= (/))

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

This theorem is referenced by:  vne0 2290  inelcm 2327  rexn0 2360  snnz 2462  prnz 2463  tpnz 2464  exss 2775  onnmin 3021  ord0eln0 3029  onne0 3039  onnev 3248  elfvdm 3753  isofrlem 3907  f1oweALT 3912  oe1m 4185  oawordeulem 4194  oa00 4199  oarec 4202  omord 4205  oewordri 4225  oeworde 4226  oeordsuc 4227  oelim2 4228  unblem1 4551  inf1 4616  noinfep 4650  zfregs 4657  aceq5lem2 4746  kmlem6 4780  alephval2 4913  addclpi 5032  mulclpi 5033  indpi 5046  1pr 5129  infmrcl 6071  flval3t 6241  eliooxrt 6388  iccsupr 6399  fseqsupcl 6526  fseqsupub 6527  seq1ublem 6911  climsup 7155  caucvglem2 7158  cvgcmpub 7185  infcvgaux1 7219  ruclem33 7543  clscld 7680  qdensere 7748  cnpco 7766  blne0 7843  caun0 7942  lmsslem 7949  bcth 8029  ghgrpilem4 8132  nvo00 8420  nmorepnf 8427  ubthlem6 8530  pilem2 8667  pilem3 8668  axgroth3 8774  projlem8 9188  shintclt 9289  chintclt 9291  hsupval2t 9295  nmoprepnf 9789  nmfnrepnf 9802  hine 10696

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-ne 1590  df-v 1815  df-dif 2052  df-nul 2284

Copyright terms: Public domain