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

Theorem neq0 3465
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 2448 . 2  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
2 n0 3464 . 2  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
31, 2bitr3i 242 1  |-  ( -.  A  =  (/)  <->  E. x  x  e.  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176   E.wex 1528    = wceq 1623    e. wcel 1684    =/= wne 2446   (/)c0 3455
This theorem is referenced by:  eq0  3469  ralidm  3557  snprc  3695  pwpw0  3763  sssn  3772  pwsnALT  3822  uni0b  3852  disjor  4007  isomin  5834  erdisj  6707  ixpprc  6837  domunsn  7011  sucdom2  7057  isinf  7076  enp1i  7093  xpfi  7128  scottex  7555  acndom  7678  axcclem  8083  axpowndlem3  8221  canthp1lem1  8274  isumltss  12307  ppttop  16744  ntreq0  16814  txindis  17328  txcon  17383  fmfnfm  17653  ptcmplem2  17747  ptcmplem3  17748  bddmulibl  19193  pf1rcl  19432  strlem1  22830  hpd  25581  fnchoice  27112  bnj1143  28195
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-nul 3456
  Copyright terms: Public domain W3C validator