Theorem neq0 4279

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 1783	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
2		eq0 4277	. . 3 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3	1, 2	xchbinxr 335	. 2 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ 𝐴 = ∅)
4	3	bicomi 223	1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2106  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-dif 3890  df-nul 4257

This theorem is referenced by:  n0  4280  ralidmOLD  4446  falseral0  4450  snprc  4653  pwpw0  4746  sssn  4759  pwsnOLD  4832  uni0b  4867  disjor  5054  rnep  5836  isomin  7208  mpoxneldm  8028  mpoxopynvov0g  8030  mpoxopxnop0  8031  erdisj  8550  ixpprc  8707  sucdom2OLD  8869  domunsn  8914  sucdom2  8989  isinf  9036  nfielex  9047  enp1i  9052  xpfi  9085  scottex  9643  acndom  9807  axcclem  10213  axpowndlem3  10355  canthp1lem1  10408  isumltss  15560  pf1rcl  21515  ppttop  22157  ntreq0  22228  txindis  22785  txconn  22840  fmfnfm  23109  ptcmplem2  23204  ptcmplem3  23205  bddmulibl  25003  g0wlk0  28019  wwlksnndef  28270  strlem1  30612  disjorf  30918  ddemeas  32204  tgoldbachgt  32643  bnj1143  32770  prv1n  33393  pibt2  35588  poimirlem25  35802  poimirlem27  35804  ineleq  36486  eqvreldisj  36727  grucollcld  41878  fnchoice  42572  founiiun0  42728  nzerooringczr  45630  mo0sn  46161  map0cor  46182