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

Theorem neq0 3644
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 2606 . 2  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
2 n0 3643 . 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 1364   E.wex 1591    e. wcel 1761    =/= wne 2604   (/)c0 3634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-v 2972  df-dif 3328  df-nul 3635
This theorem is referenced by:  eq0  3649  ralidm  3780  snprc  3936  pwpw0  4018  sssn  4028  pwsnALT  4083  uni0b  4113  disjor  4273  isomin  6025  mpt2xopynvov0g  6730  mpt2xopxnop0  6731  erdisj  7144  ixpprc  7280  domunsn  7457  sucdom2  7503  isinf  7522  nfielex  7537  enp1i  7543  xpfi  7579  scottex  8088  acndom  8217  axcclem  8622  axpowndlem3  8760  axpowndlem3OLD  8761  canthp1lem1  8815  isumltss  13307  pf1rcl  17752  ppttop  18570  ntreq0  18640  txindis  19166  txcon  19221  fmfnfm  19490  ptcmplem2  19584  ptcmplem3  19585  bddmulibl  21275  strlem1  25589  disjorf  25858  ddemeas  26588  fnchoice  29676  wwlknndef  30294  clwwlknndef  30361  bnj1143  31618
  Copyright terms: Public domain W3C validator