Theorem neq0 4310

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 2154, ax-12 2171. (Revised by Gino Giotto, 28-Jun-2024.)

Assertion

Ref	Expression
neq0	⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0

Step	Hyp	Ref	Expression
1		df-ex 1782	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
2		eq0 4308	. . 3 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3	1, 2	xchbinxr 334	. 2 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ 𝐴 = ∅)
4	3	bicomi 223	1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106  ∅c0 4287

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-dif 3916  df-nul 4288

This theorem is referenced by:  n0  4311  ralidmOLD  4478  falseral0  4482  snprc  4683  pwpw0  4778  sssn  4791  pwsnOLD  4863  uni0b  4899  disjor  5090  rnep  5887  isomin  7287  mpoxneldm  8148  mpoxopynvov0g  8150  mpoxopxnop0  8151  erdisj  8707  ixpprc  8864  sucdom2OLD  9033  domunsn  9078  sucdom2  9157  isinf  9211  isinfOLD  9212  nfielex  9224  enp1iOLD  9231  xpfiOLD  9269  scottex  9830  acndom  9996  axcclem  10402  axpowndlem3  10544  canthp1lem1  10597  isumltss  15744  pf1rcl  21752  ppttop  22394  ntreq0  22465  txindis  23022  txconn  23077  fmfnfm  23346  ptcmplem2  23441  ptcmplem3  23442  bddmulibl  25240  g0wlk0  28663  wwlksnndef  28913  strlem1  31255  disjorf  31564  ddemeas  32924  tgoldbachgt  33365  bnj1143  33491  prv1n  34112  pibt2  35961  poimirlem25  36176  poimirlem27  36178  ineleq  36888  eqvreldisj  37149  grucollcld  42662  fnchoice  43356  founiiun0  43531  nzerooringczr  46490  mo0sn  47020  map0cor  47041