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

Theorem neq0 3426
Description: A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
neq0  |-  ( -.  A  =  (/)  <->  E. x  x  e.  A )
Distinct variable group:    x, A

Proof of Theorem neq0
StepHypRef Expression
1 df-ne 2421 . 2  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
2 n0 3425 . 2  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
31, 2bitr3i 244 1  |-  ( -.  A  =  (/)  <->  E. x  x  e.  A )
Colors of variables: wff set class
Syntax hints:   -. wn 5    <-> wb 178   E.wex 1537    = wceq 1619    e. wcel 1621    =/= wne 2419   (/)c0 3416
This theorem is referenced by:  eq0  3430  ralidm  3518  snprc  3655  pwpw0  3723  sssn  3732  pwsnALT  3782  uni0b  3812  disjor  3967  isomin  5754  erdisj  6661  ixpprc  6791  domunsn  6965  sucdom2  7011  isinf  7030  enp1i  7047  xpfi  7082  scottex  7509  acndom  7632  axcclem  8037  axpowndlem3  8175  canthp1lem1  8228  isumltss  12255  ppttop  16692  ntreq0  16762  txindis  17276  txcon  17331  fmfnfm  17601  ptcmplem2  17695  ptcmplem3  17696  bddmulibl  19141  pf1rcl  19380  strlem1  22776  hpd  25522  fnchoice  27054  bnj1143  27855
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-v 2759  df-dif 3116  df-nul 3417
  Copyright terms: Public domain W3C validator