Theorem neq0 4358

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0

Step	Hyp	Ref	Expression
1		df-ex 1777	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
2		eq0 4356	. . 3 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3	1, 2	xchbinxr 335	. 2 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ 𝐴 = ∅)
4	3	bicomi 224	1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1535   = wceq 1537  ∃wex 1776   ∈ wcel 2106  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-dif 3966  df-nul 4340

This theorem is referenced by:  n0  4359  falseral0  4522  snprc  4722  pwpw0  4818  sssn  4831  uni0b  4938  disjor  5130  rnep  5940  isomin  7357  mpoxneldm  8236  mpoxopynvov0g  8238  mpoxopxnop0  8239  erdisj  8798  ixpprc  8958  sucdom2OLD  9121  domunsn  9166  sucdom2  9241  isinf  9294  isinfOLD  9295  nfielex  9305  enp1iOLD  9312  xpfiOLD  9357  scottex  9923  acndom  10089  axcclem  10495  axpowndlem3  10637  canthp1lem1  10690  isumltss  15881  nzerooringczr  21509  pf1rcl  22369  ppttop  23030  ntreq0  23101  txindis  23658  txconn  23713  fmfnfm  23982  ptcmplem2  24077  ptcmplem3  24078  bddmulibl  25889  g0wlk0  29685  wwlksnndef  29935  strlem1  32279  disjorf  32599  ssdifidlprm  33466  1arithufdlem4  33555  ddemeas  34217  tgoldbachgt  34657  bnj1143  34783  prv1n  35416  pibt2  37400  poimirlem25  37632  poimirlem27  37634  ineleq  38336  eqvreldisj  38596  grucollcld  44256  fnchoice  44967  founiiun0  45133  mo0sn  48664  map0cor  48685