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

Theorem neq0 3466
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 2449 . 2  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
2 n0 3465 . 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 1529    = wceq 1624    e. wcel 1685    =/= wne 2447   (/)c0 3456
This theorem is referenced by:  eq0  3470  ralidm  3558  snprc  3696  pwpw0  3764  sssn  3773  pwsnALT  3823  uni0b  3853  disjor  4008  isomin  5795  erdisj  6702  ixpprc  6832  domunsn  7006  sucdom2  7052  isinf  7071  enp1i  7088  xpfi  7123  scottex  7550  acndom  7673  axcclem  8078  axpowndlem3  8216  canthp1lem1  8269  isumltss  12301  ppttop  16738  ntreq0  16808  txindis  17322  txcon  17377  fmfnfm  17647  ptcmplem2  17741  ptcmplem3  17742  bddmulibl  19187  pf1rcl  19426  strlem1  22822  hpd  25568  fnchoice  27099  bnj1143  28089
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-v 2791  df-dif 3156  df-nul 3457
  Copyright terms: Public domain W3C validator