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

Theorem neq0 3625
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 2595 . 2  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
2 n0 3624 . 2  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
31, 2bitr3i 243 1  |-  ( -.  A  =  (/)  <->  E. x  x  e.  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177   E.wex 1550    = wceq 1652    e. wcel 1725    =/= wne 2593   (/)c0 3615
This theorem is referenced by:  eq0  3629  ralidm  3718  snprc  3858  pwpw0  3933  sssn  3944  pwsnALT  3997  uni0b  4027  disjor  4183  isomin  6043  mpt2xopynvov0g  6451  mpt2xopxnop0  6452  erdisj  6938  ixpprc  7069  domunsn  7243  sucdom2  7289  isinf  7308  nfielex  7323  enp1i  7329  xpfi  7364  scottex  7793  acndom  7916  axcclem  8321  axpowndlem3  8458  canthp1lem1  8511  isumltss  12611  ppttop  17054  ntreq0  17124  txindis  17649  txcon  17704  fmfnfm  17973  ptcmplem2  18067  ptcmplem3  18068  bddmulibl  19713  pf1rcl  19952  strlem1  23736  disjorf  24004  fnchoice  27609  bnj1143  28913
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-v 2945  df-dif 3310  df-nul 3616
  Copyright terms: Public domain W3C validator