Theorem neq0 4293

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∅c0 4274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-dif 3893  df-nul 4275

This theorem is referenced by:  n0  4294  falseral0OLD  4456  snprc  4662  pwpw0  4757  sssn  4770  uni0b  4877  disjor  5068  rnep  5876  isomin  7285  mpoxneldm  8155  mpoxopynvov0g  8157  mpoxopxnop0  8158  erdisj  8694  ixpprc  8860  domunsn  9058  sucdom2  9130  isinf  9168  nfielex  9177  scottex  9800  acndom  9964  axcclem  10370  axpowndlem3  10513  canthp1lem1  10566  isumltss  15804  nzerooringczr  21470  pf1rcl  22324  ppttop  22982  ntreq0  23052  txindis  23609  txconn  23664  fmfnfm  23933  ptcmplem2  24028  ptcmplem3  24029  bddmulibl  25816  g0wlk0  29734  wwlksnndef  29988  strlem1  32336  disjorf  32664  ssdifidlprm  33533  1arithufdlem4  33622  ddemeas  34396  tgoldbachgt  34823  bnj1143  34948  prv1n  35629  pibt2  37747  poimirlem25  37980  poimirlem27  37982  ineleq  38689  dmcnvep  38723  eqvreldisj  39033  grucollcld  44705  relpmin  45397  fnchoice  45478  founiiun0  45638  mo0sn  49303  map0cor  49342  termchom  49975