Theorem n0i 4286

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

Assertion

Ref	Expression
n0i	⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)

Proof of Theorem n0i

Step	Hyp	Ref	Expression
1		nel02 4285	. 2 ⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴)
2	1	con2i 140	1 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2145  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-dif 3902  df-nul 4280

This theorem is used by:  ne0i  4287  n0ii  4289  oprcl  4859  disjss3  5102  elfvdm  6919  mptrcl  7003  isomin  7345  ovrcl  7461  elfvov1  7462  elfvov2  7463  oalimcl  8568  omlimcl  8586  nnaordex2  8648  oaabs2  8658  ecexr  8722  elpmi  8866  elmapex  8868  pmresg  8898  pmsspw  8905  ixpssmap2g  8955  ixpssmapg  8956  resixpfo  8964  php3  9224  cantnfp1lem2  9680  cantnflem1  9690  cnfcom2lem  9702  rankxplim2  9897  rankxplim3  9898  cardlim  10053  alephnbtwn  10150  ttukeylem5  10591  r1wunlim  10822  ssnn0fi  14128  ruclem13  16410  ramtub  17190  elbasfv  17393  elbasov  17394  restsspw  17602  homarcl  18203  grpidval  18840  odlem2  19753  efgrelexlema  19963  subcmn  20051  dvdsrval  20591  ssdifidllem  21640  elocv  21974  pf1rcl  22667  matrcl  22727  0top  23301  ppttop  23325  pptbas  23326  restrcl  23475  ssrest  23494  iscnp2  23557  lmmo  23698  zfbas  24215  rnelfmlem  24271  isfcls  24328  isnghm  25042  iscau2  25598  itg2cnlem1  26082  itgsubstlem  26368  dchrrcl  27567  clwwlknnn  30624  0ringsubrg  33812  ssmxidllem  33998  eulerpartlemgvv  35008  indispconn  35999  cvmtop1  36025  cvmtop2  36026  mrsub0  36281  mrsubf  36282  mrsubccat  36283  mrsubcn  36284  mrsubco  36286  mrsubvrs  36287  msubf  36297  mclsrcl  36326  funpartlem  36706  tailfb  37165  nlpineqsn  38331  atbase  40346  llnbase  40566  lplnbase  40591  lvolbase  40635  osumcllem4N  41016  pexmidlem1N  41027  lhpbase  41055  mapco2g  43724  wepwsolem  44048  onov0suclim  44275  uneqsn  45024  relpmin  45941  ssfiunibd  46324  hoicvr  47557  0nelsetpreimafv  48471  termchomn0  50591