Theorem neq0 4306

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0

Step	Hyp	Ref	Expression
1		df-ex 1810	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
2		eq0 4304	. . 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 1809   ∈ wcel 2143  ∅c0 4286

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-dif 3908  df-nul 4287

This theorem is used by:  n0  4307  falseral0OLD  4476  snprc  4683  pwpw0  4779  sssn  4792  uni0b  4899  disjor  5091  rnep  5917  isomin  7335  mpoxneldm  8204  mpoxopynvov0g  8206  mpoxopxnop0  8207  erdisj  8748  ixpprc  8913  domunsn  9111  sucdom2  9183  isinf  9221  nfielex  9230  scottex  9858  scottexOLD  9859  acndom  10040  axcclem  10445  axpowndlem3  10588  canthp1lem1  10641  isumltss  15907  ssdifidlprm  21495  nzerooringczr  21639  pf1rcl  22518  ppttop  23173  ntreq0  23243  txindis  23800  txconn  23855  fmfnfm  24124  ptcmplem2  24219  ptcmplem3  24220  bddmulibl  26007  g0wlk0  30009  wwlksnndef  30263  strlem1  32611  disjorf  32933  1arithufdlem4  33846  ddemeas  34635  tgoldbachgt  35059  bnj1143  35187  rankscottu  35531  prv1n  35931  pibt2  38091  poimirlem25  38324  poimirlem27  38326  ineleq  39031  dmcnvep  39065  eqvreldisj  39375  grucollcld  44998  relpmin  45689  fnchoice  45777  founiiun0  45936  mo0sn  49622  map0cor  49661  termchom  50294