Theorem n0i 4281

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 4280	. 2 ⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴)
2	1	con2i 139	1 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2114  ∅c0 4274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-dif 3893  df-nul 4275

This theorem is referenced by:  ne0i  4282  n0ii  4284  oprcl  4843  disjss3  5085  elfvdm  6869  mptrcl  6952  isomin  7286  ovrcl  7402  elfvov1  7403  elfvov2  7404  oalimcl  8489  omlimcl  8507  nnaordex2  8569  oaabs2  8579  ecexr  8642  elpmi  8787  elmapex  8789  pmresg  8812  pmsspw  8819  ixpssmap2g  8869  ixpssmapg  8870  resixpfo  8878  php3  9137  cantnfp1lem2  9594  cantnflem1  9604  cnfcom2lem  9616  rankxplim2  9798  rankxplim3  9799  cardlim  9890  alephnbtwn  9987  ttukeylem5  10429  r1wunlim  10654  ssnn0fi  13941  ruclem13  16203  ramtub  16977  elbasfv  17179  elbasov  17180  restsspw  17388  homarcl  17989  grpidval  18623  odlem2  19508  efgrelexlema  19718  subcmn  19806  dvdsrval  20335  elocv  21661  pf1rcl  22327  matrcl  22390  0top  22961  ppttop  22985  pptbas  22986  restrcl  23135  ssrest  23154  iscnp2  23217  lmmo  23358  zfbas  23874  rnelfmlem  23930  isfcls  23987  isnghm  24701  iscau2  25257  itg2cnlem1  25741  itgsubstlem  26028  dchrrcl  27220  clwwlknnn  30121  0ringsubrg  33330  ssdifidllem  33534  ssmxidllem  33551  eulerpartlemgvv  34539  indispconn  35435  cvmtop1  35461  cvmtop2  35462  mrsub0  35717  mrsubf  35718  mrsubccat  35719  mrsubcn  35720  mrsubco  35722  mrsubvrs  35723  msubf  35733  mclsrcl  35762  funpartlem  36143  tailfb  36578  nlpineqsn  37741  atbase  39752  llnbase  39972  lplnbase  39997  lvolbase  40041  osumcllem4N  40422  pexmidlem1N  40433  lhpbase  40461  mapco2g  43163  wepwsolem  43491  onov0suclim  43723  uneqsn  44473  relpmin  45400  ssfiunibd  45763  hoicvr  46997  0nelsetpreimafv  47865  termchomn0  49974