MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neq0 Structured version   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  |-  ( -.  A  =  (/)  <->  E. x  x  e.  A )
Distinct variable group:    x, A

Proof of Theorem neq0
StepHypRef Expression
1 df-ne 2664 . 2  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
2 n0 3794 . 2  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
31, 2bitr3i 251 1  |-  ( -.  A  =  (/)  <->  E. x  x  e.  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    = wceq 1379   E.wex 1596    e. wcel 1767    =/= wne 2662   (/)c0 3785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3115  df-dif 3479  df-nul 3786
This theorem is referenced by:  eq0  3800  ralidm  3931  snprc  4091  pwpw0  4175  sssn  4185  pwsnALT  4240  uni0b  4270  disjor  4431  isomin  6221  mpt2xopynvov0g  6942  mpt2xopxnop0  6943  erdisj  7359  ixpprc  7490  domunsn  7667  sucdom2  7714  isinf  7733  nfielex  7748  enp1i  7755  xpfi  7791  scottex  8303  acndom  8432  axcclem  8837  axpowndlem3  8975  axpowndlem3OLD  8976  canthp1lem1  9030  isumltss  13623  pf1rcl  18184  ppttop  19302  ntreq0  19372  txindis  19898  txcon  19953  fmfnfm  20222  ptcmplem2  20316  ptcmplem3  20317  bddmulibl  22008  wwlknndef  24441  clwwlknndef  24477  strlem1  26873  disjorf  27141  ddemeas  27876  fnchoice  31010  bnj1143  32946
  Copyright terms: Public domain W3C validator