MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neq0 Unicode version

Theorem neq0 3795
Description: A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
neq0
Distinct variable group:   ,

Proof of Theorem neq0
StepHypRef Expression
1 df-ne 2654 . 2
2 n0 3794 . 2
31, 2bitr3i 251 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184  =wceq 1395  E.wex 1612  e.wcel 1818  =/=wne 2652   c0 3784
This theorem is referenced by:  eq0  3800  ralidm  3933  snprc  4093  pwpw0  4178  sssn  4188  pwsnALT  4244  uni0b  4274  disjor  4436  isomin  6233  mpt2xopynvov0g  6961  mpt2xopxnop0  6962  erdisj  7378  ixpprc  7510  domunsn  7687  sucdom2  7734  isinf  7753  nfielex  7768  enp1i  7775  xpfi  7811  scottex  8324  acndom  8453  axcclem  8858  axpowndlem3  8996  axpowndlem3OLD  8997  canthp1lem1  9051  isumltss  13660  pf1rcl  18385  ppttop  19508  ntreq0  19578  txindis  20135  txcon  20190  fmfnfm  20459  ptcmplem2  20553  ptcmplem3  20554  bddmulibl  22245  wwlknndef  24737  wlk0  24761  clwwlknndef  24773  strlem1  27169  disjorf  27440  ddemeas  28208  fnchoice  31404  nzerooringczr  32880  bnj1143  33849
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-nul 3785
  Copyright terms: Public domain W3C validator