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 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 4304	. . 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 4287

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 3906  df-nul 4288

This theorem is referenced by:  n0  4307  falseral0OLD  4470  snprc  4676  pwpw0  4771  sssn  4784  uni0b  4891  disjor  5082  rnep  5884  isomin  7293  mpoxneldm  8164  mpoxopynvov0g  8166  mpoxopxnop0  8167  erdisj  8703  ixpprc  8869  domunsn  9067  sucdom2  9139  isinf  9177  nfielex  9186  scottex  9809  acndom  9973  axcclem  10379  axpowndlem3  10522  canthp1lem1  10575  isumltss  15783  nzerooringczr  21447  pf1rcl  22305  ppttop  22963  ntreq0  23033  txindis  23590  txconn  23645  fmfnfm  23914  ptcmplem2  24009  ptcmplem3  24010  bddmulibl  25808  g0wlk0  29736  wwlksnndef  29990  strlem1  32337  disjorf  32665  ssdifidlprm  33550  1arithufdlem4  33639  ddemeas  34413  tgoldbachgt  34840  bnj1143  34965  prv1n  35644  pibt2  37666  poimirlem25  37890  poimirlem27  37892  ineleq  38599  dmcnvep  38633  eqvreldisj  38943  grucollcld  44610  relpmin  45302  fnchoice  45383  founiiun0  45543  mo0sn  49169  map0cor  49208  termchom  49841