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

Theorem neq0 3772
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 2620 . 2  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
2 n0 3771 . 2  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
31, 2bitr3i 254 1  |-  ( -.  A  =  (/)  <->  E. x  x  e.  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187    = wceq 1437   E.wex 1659    e. wcel 1868    =/= wne 2618   (/)c0 3761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-v 3083  df-dif 3439  df-nul 3762
This theorem is referenced by:  eq0  3777  ralidm  3901  snprc  4060  pwpw0  4145  sssn  4155  pwsnALT  4211  uni0b  4241  disjor  4405  isomin  6239  mpt2xopynvov0g  6964  mpt2xopxnop0  6965  erdisj  7415  ixpprc  7547  domunsn  7724  sucdom2  7770  isinf  7787  nfielex  7802  enp1i  7808  xpfi  7844  scottex  8357  acndom  8482  axcclem  8887  axpowndlem3  9024  canthp1lem1  9077  isumltss  13891  pf1rcl  18922  ppttop  20006  ntreq0  20077  txindis  20633  txcon  20688  fmfnfm  20957  ptcmplem2  21052  ptcmplem3  21053  bddmulibl  22780  wwlknndef  25448  wlk0  25472  clwwlknndef  25484  strlem1  27886  disjorf  28176  ddemeas  29052  bnj1143  29595  poimirlem25  31876  poimirlem27  31878  fnchoice  37208  founiiun0  37312  nzerooringczr  39260
  Copyright terms: Public domain W3C validator