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

Theorem neq0 4131
Description: A class is not empty if and only if it 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 2948 . 2 𝑥𝐴
21neq0f 4128 1 𝐴 = ∅ ↔ ∃𝑥 𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197   = wceq 1637  wex 1859  wcel 2156  c0 4116
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-dif 3772  df-nul 4117
This theorem is referenced by:  ralidm  4270  falseral0  4274  snprc  4444  pwpw0  4534  sssn  4547  pwsnALT  4623  uni0b  4657  disjor  4826  isomin  6807  mpt2xneldm  7569  mpt2xopynvov0g  7571  mpt2xopxnop0  7572  erdisj  8025  ixpprc  8162  domunsn  8345  sucdom2  8391  isinf  8408  nfielex  8424  enp1i  8430  xpfi  8466  scottex  8991  acndom  9153  axcclem  9560  axpowndlem3  9702  canthp1lem1  9755  isumltss  14798  pf1rcl  19917  ppttop  21022  ntreq0  21092  txindis  21648  txconn  21703  fmfnfm  21972  ptcmplem2  22067  ptcmplem3  22068  bddmulibl  23818  g0wlk0  26775  wwlksnndef  27041  strlem1  29436  disjorf  29716  ddemeas  30623  tgoldbachgt  31065  bnj1143  31182  poimirlem25  33745  poimirlem27  33747  ineleq  34430  fnchoice  39679  founiiun0  39863  nzerooringczr  42637
  Copyright terms: Public domain W3C validator