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

Theorem neq0 4261
 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 2158, ax-12 2175. (Revised by Gino Giotto, 28-Jun-2024.)
Assertion
Ref Expression
neq0 𝐴 = ∅ ↔ ∃𝑥 𝑥𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0
StepHypRef Expression
1 df-ex 1782 . . 3 (∃𝑥 𝑥𝐴 ↔ ¬ ∀𝑥 ¬ 𝑥𝐴)
2 eq0 4260 . . 3 (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥𝐴)
31, 2xchbinxr 338 . 2 (∃𝑥 𝑥𝐴 ↔ ¬ 𝐴 = ∅)
43bicomi 227 1 𝐴 = ∅ ↔ ∃𝑥 𝑥𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∅c0 4245 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-dif 3885  df-nul 4246 This theorem is referenced by:  n0  4262  ralidm  4415  falseral0  4419  snprc  4615  pwpw0  4708  sssn  4721  pwsnOLD  4796  uni0b  4829  disjor  5013  rnep  5766  isomin  7076  mpoxneldm  7876  mpoxopynvov0g  7878  mpoxopxnop0  7879  erdisj  8339  ixpprc  8481  sucdom2  8625  domunsn  8666  isinf  8730  nfielex  8746  enp1i  8752  xpfi  8788  scottex  9313  acndom  9477  axcclem  9883  axpowndlem3  10025  canthp1lem1  10078  isumltss  15212  pf1rcl  21011  ppttop  21650  ntreq0  21720  txindis  22277  txconn  22332  fmfnfm  22601  ptcmplem2  22696  ptcmplem3  22697  bddmulibl  24480  g0wlk0  27482  wwlksnndef  27732  strlem1  30074  disjorf  30383  ddemeas  31668  tgoldbachgt  32107  bnj1143  32235  prv1n  32854  pibt2  34901  poimirlem25  35149  poimirlem27  35151  ineleq  35835  eqvreldisj  36076  grucollcld  41055  fnchoice  41745  founiiun0  41903  nzerooringczr  44780
 Copyright terms: Public domain W3C validator