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

Theorem neq0 4352
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.) Avoid ax-11 2157, ax-12 2177. (Revised by GG, 28-Jun-2024.)
Assertion
Ref Expression
neq0 𝐴 = ∅ ↔ ∃𝑥 𝑥𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0
StepHypRef Expression
1 df-ex 1780 . . 3 (∃𝑥 𝑥𝐴 ↔ ¬ ∀𝑥 ¬ 𝑥𝐴)
2 eq0 4350 . . 3 (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥𝐴)
31, 2xchbinxr 335 . 2 (∃𝑥 𝑥𝐴 ↔ ¬ 𝐴 = ∅)
43bicomi 224 1 𝐴 = ∅ ↔ ∃𝑥 𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wal 1538   = wceq 1540  wex 1779  wcel 2108  c0 4333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-dif 3954  df-nul 4334
This theorem is referenced by:  n0  4353  falseral0  4516  snprc  4717  pwpw0  4813  sssn  4826  uni0b  4933  disjor  5125  rnep  5937  isomin  7357  mpoxneldm  8237  mpoxopynvov0g  8239  mpoxopxnop0  8240  erdisj  8799  ixpprc  8959  sucdom2OLD  9122  domunsn  9167  sucdom2  9243  isinf  9296  isinfOLD  9297  nfielex  9307  enp1iOLD  9314  xpfiOLD  9359  scottex  9925  acndom  10091  axcclem  10497  axpowndlem3  10639  canthp1lem1  10692  isumltss  15884  nzerooringczr  21491  pf1rcl  22353  ppttop  23014  ntreq0  23085  txindis  23642  txconn  23697  fmfnfm  23966  ptcmplem2  24061  ptcmplem3  24062  bddmulibl  25874  g0wlk0  29670  wwlksnndef  29925  strlem1  32269  disjorf  32592  ssdifidlprm  33486  1arithufdlem4  33575  ddemeas  34237  tgoldbachgt  34678  bnj1143  34804  prv1n  35436  pibt2  37418  poimirlem25  37652  poimirlem27  37654  ineleq  38355  eqvreldisj  38615  grucollcld  44279  relpmin  44973  fnchoice  45034  founiiun0  45195  mo0sn  48735  map0cor  48764
  Copyright terms: Public domain W3C validator