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

Theorem neq0 3647
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 2608 . 2  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
2 n0 3646 . 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 1369   E.wex 1586    e. wcel 1756    =/= wne 2606   (/)c0 3637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-v 2974  df-dif 3331  df-nul 3638
This theorem is referenced by:  eq0  3652  ralidm  3783  snprc  3939  pwpw0  4021  sssn  4031  pwsnALT  4086  uni0b  4116  disjor  4276  isomin  6028  mpt2xopynvov0g  6731  mpt2xopxnop0  6732  erdisj  7148  ixpprc  7284  domunsn  7461  sucdom2  7507  isinf  7526  nfielex  7541  enp1i  7547  xpfi  7583  scottex  8092  acndom  8221  axcclem  8626  axpowndlem3  8764  axpowndlem3OLD  8765  canthp1lem1  8819  isumltss  13311  pf1rcl  17783  ppttop  18611  ntreq0  18681  txindis  19207  txcon  19262  fmfnfm  19531  ptcmplem2  19625  ptcmplem3  19626  bddmulibl  21316  strlem1  25654  disjorf  25923  ddemeas  26652  fnchoice  29751  wwlknndef  30369  clwwlknndef  30436  bnj1143  31784
  Copyright terms: Public domain W3C validator