Theorem neq0 4352

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ∅c0 4333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-dif 3954  df-nul 4334

This theorem is referenced by:  n0  4353  falseral0  4516  snprc  4717  pwpw0  4813  sssn  4826  uni0b  4933  disjor  5125  rnep  5937  isomin  7357  mpoxneldm  8237  mpoxopynvov0g  8239  mpoxopxnop0  8240  erdisj  8799  ixpprc  8959  sucdom2OLD  9122  domunsn  9167  sucdom2  9243  isinf  9296  isinfOLD  9297  nfielex  9307  enp1iOLD  9314  xpfiOLD  9359  scottex  9925  acndom  10091  axcclem  10497  axpowndlem3  10639  canthp1lem1  10692  isumltss  15884  nzerooringczr  21491  pf1rcl  22353  ppttop  23014  ntreq0  23085  txindis  23642  txconn  23697  fmfnfm  23966  ptcmplem2  24061  ptcmplem3  24062  bddmulibl  25874  g0wlk0  29670  wwlksnndef  29925  strlem1  32269  disjorf  32592  ssdifidlprm  33486  1arithufdlem4  33575  ddemeas  34237  tgoldbachgt  34678  bnj1143  34804  prv1n  35436  pibt2  37418  poimirlem25  37652  poimirlem27  37654  ineleq  38355  eqvreldisj  38615  grucollcld  44279  relpmin  44973  fnchoice  45034  founiiun0  45195  mo0sn  48735  map0cor  48764