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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0

Step	Hyp	Ref	Expression
1		df-ex 1803	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
2		eq0 4305	. . 3 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3	1, 2	xchbinxr 338	. 2 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ 𝐴 = ∅)
4	3	bicomi 227	1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1561   = wceq 1563  ∃wex 1802   ∈ wcel 2145  ∅c0 4288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-dif 3910  df-nul 4289

This theorem is referenced by:  n0  4308  falseral0OLD  4472  snprc  4679  pwpw0  4774  sssn  4787  uni0b  4895  disjor  5087  rnep  5908  isomin  7325  mpoxneldm  8196  mpoxopynvov0g  8198  mpoxopxnop0  8199  erdisj  8740  ixpprc  8905  domunsn  9103  sucdom2  9175  isinf  9213  nfielex  9222  scottex  9847  acndom  10023  axcclem  10429  axpowndlem3  10572  canthp1lem1  10625  isumltss  15892  ssdifidlprm  21446  nzerooringczr  21590  pf1rcl  22470  ppttop  23125  ntreq0  23195  txindis  23752  txconn  23807  fmfnfm  24076  ptcmplem2  24171  ptcmplem3  24172  bddmulibl  25959  g0wlk0  29909  wwlksnndef  30163  strlem1  32511  disjorf  32834  1arithufdlem4  33754  ddemeas  34543  tgoldbachgt  34967  bnj1143  35095  prv1n  35794  pibt2  37923  poimirlem25  38156  poimirlem27  38158  ineleq  38865  dmcnvep  38899  eqvreldisj  39209  grucollcld  44834  relpmin  45526  fnchoice  45607  founiiun0  45766  mo0sn  49445  map0cor  49484  termchom  50117