Theorem neq0 4292

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 4290	. . 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 4273

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 2708

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 2715  df-cleq 2728  df-dif 3892  df-nul 4274

This theorem is referenced by:  n0  4293  falseral0OLD  4455  snprc  4661  pwpw0  4756  sssn  4769  uni0b  4876  disjor  5067  rnep  5882  isomin  7292  mpoxneldm  8162  mpoxopynvov0g  8164  mpoxopxnop0  8165  erdisj  8701  ixpprc  8867  domunsn  9065  sucdom2  9137  isinf  9175  nfielex  9184  scottex  9809  acndom  9973  axcclem  10379  axpowndlem3  10522  canthp1lem1  10575  isumltss  15813  nzerooringczr  21460  pf1rcl  22314  ppttop  22972  ntreq0  23042  txindis  23599  txconn  23654  fmfnfm  23923  ptcmplem2  24018  ptcmplem3  24019  bddmulibl  25806  g0wlk0  29719  wwlksnndef  29973  strlem1  32321  disjorf  32649  ssdifidlprm  33518  1arithufdlem4  33607  ddemeas  34380  tgoldbachgt  34807  bnj1143  34932  prv1n  35613  pibt2  37733  poimirlem25  37966  poimirlem27  37968  ineleq  38675  dmcnvep  38709  eqvreldisj  39019  grucollcld  44687  relpmin  45379  fnchoice  45460  founiiun0  45620  mo0sn  49291  map0cor  49330  termchom  49963