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

Theorem neq0 3777
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 2638 . 2  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
2 n0 3776 . 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 1381   E.wex 1597    e. wcel 1802    =/= wne 2636   (/)c0 3767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-v 3095  df-dif 3461  df-nul 3768
This theorem is referenced by:  eq0  3782  ralidm  3914  snprc  4074  pwpw0  4159  sssn  4169  pwsnALT  4225  uni0b  4255  disjor  4417  isomin  6214  mpt2xopynvov0g  6940  mpt2xopxnop0  6941  erdisj  7357  ixpprc  7488  domunsn  7665  sucdom2  7712  isinf  7731  nfielex  7746  enp1i  7753  xpfi  7789  scottex  8301  acndom  8430  axcclem  8835  axpowndlem3  8973  axpowndlem3OLD  8974  canthp1lem1  9028  isumltss  13634  pf1rcl  18253  ppttop  19374  ntreq0  19444  txindis  20001  txcon  20056  fmfnfm  20325  ptcmplem2  20419  ptcmplem3  20420  bddmulibl  22111  wwlknndef  24602  wlk0  24626  clwwlknndef  24638  strlem1  27034  disjorf  27305  ddemeas  28074  fnchoice  31351  bnj1143  33556
  Copyright terms: Public domain W3C validator