Theorem ne0i 2286

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 2285	. 2 |- (B e. A -> -. A = (/))
2		df-ne 1587	. 2 |- (A =/= (/) <-> -. A = (/))
3	1, 2	sylibr 200	1 |- (B e. A -> A =/= (/))

Syntax hints:  -. wn 2   -> wi 3   = wceq 956   e. wcel 958   =/= wne 1585  (/)c0 2280

This theorem is referenced by:  inelcm 2323  rexn0 2356  snnz 2458  prnz 2459  tpnz 2460  exss 2769  onnmin 3015  ord0eln0 3023  onne0 3033  onnev 3242  elfvdm 3747  isofrlem 3901  f1oweALT 3906  oe1m 4179  oawordeulem 4188  oa00 4193  oarec 4196  omord 4199  oewordri 4219  oeworde 4220  oeordsuc 4221  oelim2 4222  unblem1 4540  inf1 4607  noinfep 4640  zfregs 4647  aceq5lem2 4736  kmlem6 4770  alephval2 4902  addclpi 5020  mulclpi 5021  indpi 5034  1pr 5117  infmrcl 6069  flval3t 6239  eliooxrt 6387  iccsupr 6398  fseqsupcl 6525  fseqsupub 6526  seq1ublem 6911  climsup 7155  caucvglem2 7158  cvgcmpub 7185  infcvgaux1 7219  ruclem33 7542  clscld 7683  qdensere 7751  cnpco 7769  blne0 7846  caun0 7945  lmsslem 7952  bcth 8032  ghgrpilem4 8136  nvo00 8424  nmorepnf 8431  ubthlem6 8534  pilem2 8672  pilem3 8673  axgroth3 8779  projlem8 9193  shintclt 9294  chintclt 9296  hsupval2t 9300  nmoprepnf 9794  nmfnrepnf 9807  efilcp 10572  efilcpOLD 10573  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  relrded 10675  relrcat 10696  hine 10725

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-nul 2281

Copyright terms: Public domain