Theorem neq0 4298

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wal 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-dif 4047  df-nul 4279

This theorem is used by:  n0  4299  falseral0OLD  4470  snprc  4674  sssn  4781  pwpw0  4830  uni0b  4893  disjor  5084  rnep  5908  isomin  7345  mpoxneldm  8232  mpoxopynvov0g  8234  mpoxopxnop0  8235  erdisj  8778  ixpprc  8950  domunsn  9149  sucdom2  9221  isinf  9259  nfielex  9268  scottex  9936  scottexOLD  9937  acndom  10133  axcclem  10538  axpowndlem3  10687  canthp1lem1  10740  isumltss  16022  ssdifidlprm  21647  nzerooringczr  21791  pf1rcl  22672  ppttop  23330  ntreq0  23400  txindis  23958  txconn  24013  fmfnfm  24282  ptcmplem2  24377  ptcmplem3  24378  bddmulibl  26164  g0wlk0  30236  wwlksnndef  30499  strlem1  32857  disjorf  33220  1arithufdlem4  34125  ddemeas  34915  tgoldbachgt  35338  bnj1143  35466  rankscottu  35807  prv1n  36282  pibt2  38433  poimirlem25  38656  poimirlem27  38658  ineleq  39379  dmcnvep  39413  eqvreldisj  39723  grucollcld  45337  relpmin  46035  fnchoice  46139  founiiun0  46298  mo0sn  50020  map0cor  50059  termchom  50716