Theorem neq0 4302

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 2194, ax-12 2215. (Revised by GG, 28-Jun-2024.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0

Step	Hyp	Ref	Expression
1		df-ex 1813	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
2		eq0 4300	. . 3 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3	1, 2	xchbinxr 338	. 2 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ 𝐴 = ∅)
4	3	bicomi 227	1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∅c0 4282

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-dif 3905  df-nul 4283

This theorem is used by:  n0  4303  falseral0OLD  4474  snprc  4681  pwpw0  4777  sssn  4790  uni0b  4897  disjor  5089  rnep  5915  isomin  7342  mpoxneldm  8214  mpoxopynvov0g  8216  mpoxopxnop0  8217  erdisj  8758  ixpprc  8930  domunsn  9129  sucdom2  9201  isinf  9239  nfielex  9248  scottex  9876  scottexOLD  9877  acndom  10058  axcclem  10463  axpowndlem3  10612  canthp1lem1  10665  isumltss  15941  ssdifidlprm  21555  nzerooringczr  21699  pf1rcl  22580  ppttop  23238  ntreq0  23308  txindis  23866  txconn  23921  fmfnfm  24190  ptcmplem2  24285  ptcmplem3  24286  bddmulibl  26073  g0wlk0  30118  wwlksnndef  30381  strlem1  32739  disjorf  33060  1arithufdlem4  33965  ddemeas  34755  tgoldbachgt  35179  bnj1143  35307  rankscottu  35644  prv1n  36018  pibt2  38179  poimirlem25  38402  poimirlem27  38404  ineleq  39110  dmcnvep  39144  eqvreldisj  39454  grucollcld  45092  relpmin  45783  fnchoice  45871  founiiun0  46030  mo0sn  49752  map0cor  49791  termchom  50422