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 2197, ax-12 2216. (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 2147  ∅c0 4281

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-dif 4050  df-nul 4282

This theorem is used by:  n0  4303  falseral0OLD  4474  snprc  4678  sssn  4785  pwpw0  4834  uni0b  4897  disjor  5088  rnep  5916  isomin  7368  mpoxneldm  8257  mpoxopynvov0g  8259  mpoxopxnop0  8260  erdisj  8803  ixpprc  8975  domunsn  9174  sucdom2  9246  isinf  9284  nfielex  9293  scottex  9960  scottexOLD  9961  acndom  10157  axcclem  10562  axpowndlem3  10711  canthp1lem1  10764  isumltss  16046  ssdifidlprm  21672  nzerooringczr  21816  pf1rcl  22697  ppttop  23355  ntreq0  23425  txindis  23983  txconn  24038  fmfnfm  24307  ptcmplem2  24402  ptcmplem3  24403  bddmulibl  26189  g0wlk0  30261  wwlksnndef  30524  strlem1  32882  disjorf  33245  1arithufdlem4  34149  ddemeas  34939  tgoldbachgt  35362  bnj1143  35490  rankscottu  35839  prv1n  36363  pibt2  38532  poimirlem25  38755  poimirlem27  38757  ineleq  39478  dmcnvep  39512  eqvreldisj  39822  grucollcld  45436  relpmin  46137  fnchoice  46251  founiiun0  46410  mo0sn  50132  map0cor  50171  termchom  50828