Theorem neq0 4307

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 4305	. . 3 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3	1, 2	xchbinxr 338	. 2 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ 𝐴 = ∅)
4	3	bicomi 227	1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1568   = wceq 1570  ∃wex 1809   ∈ wcel 2143  ∅c0 4287

This theorem was proved from 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 theorem 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 3909  df-nul 4288

This theorem is referenced by:  n0  4308  falseral0OLD  4477  snprc  4684  pwpw0  4780  sssn  4793  uni0b  4900  disjor  5092  rnep  5919  isomin  7337  mpoxneldm  8209  mpoxopynvov0g  8211  mpoxopxnop0  8212  erdisj  8753  ixpprc  8918  domunsn  9116  sucdom2  9188  isinf  9226  nfielex  9235  scottex  9860  acndom  10036  axcclem  10442  axpowndlem3  10585  canthp1lem1  10638  isumltss  15904  ssdifidlprm  21467  nzerooringczr  21611  pf1rcl  22490  ppttop  23145  ntreq0  23215  txindis  23772  txconn  23827  fmfnfm  24096  ptcmplem2  24191  ptcmplem3  24192  bddmulibl  25979  g0wlk0  29978  wwlksnndef  30232  strlem1  32580  disjorf  32902  1arithufdlem4  33815  ddemeas  34604  tgoldbachgt  35028  bnj1143  35156  rankscottu  35501  prv1n  35901  pibt2  38041  poimirlem25  38274  poimirlem27  38276  ineleq  38981  dmcnvep  39015  eqvreldisj  39325  grucollcld  44950  relpmin  45641  fnchoice  45729  founiiun0  45888  mo0sn  49571  map0cor  49610  termchom  50243