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

Theorem neq0 3963
 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 𝐴 = ∅ ↔ ∃𝑥 𝑥𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0
StepHypRef Expression
1 nfcv 2793 . 2 𝑥𝐴
21neq0f 3959 1 𝐴 = ∅ ↔ ∃𝑥 𝑥𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 196   = wceq 1523  ∃wex 1744   ∈ wcel 2030  ∅c0 3948 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-nul 3949 This theorem is referenced by:  ralidm  4108  falseral0  4114  snprc  4285  pwpw0  4376  sssn  4390  pwsnALT  4461  uni0b  4495  disjor  4666  isomin  6627  mpt2xneldm  7383  mpt2xopynvov0g  7385  mpt2xopxnop0  7386  erdisj  7837  ixpprc  7971  domunsn  8151  sucdom2  8197  isinf  8214  nfielex  8230  enp1i  8236  xpfi  8272  scottex  8786  acndom  8912  axcclem  9317  axpowndlem3  9459  canthp1lem1  9512  isumltss  14624  pf1rcl  19761  ppttop  20859  ntreq0  20929  txindis  21485  txconn  21540  fmfnfm  21809  ptcmplem2  21904  ptcmplem3  21905  bddmulibl  23650  g0wlk0  26604  wwlksnndef  26868  strlem1  29237  disjorf  29518  ddemeas  30427  tgoldbachgt  30869  bnj1143  30987  poimirlem25  33564  poimirlem27  33566  ineleq  34259  fnchoice  39502  founiiun0  39691  nzerooringczr  42397
 Copyright terms: Public domain W3C validator