Theorem neq0 4260

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 2158, ax-12 2175. (Revised by Gino Giotto, 28-Jun-2024.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1541   = wceq 1543  ∃wex 1787   ∈ wcel 2110  ∅c0 4237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-dif 3869  df-nul 4238

This theorem is referenced by:  n0  4261  ralidmOLD  4427  falseral0  4431  snprc  4633  pwpw0  4726  sssn  4739  pwsnOLD  4812  uni0b  4847  disjor  5033  rnep  5796  isomin  7146  mpoxneldm  7954  mpoxopynvov0g  7956  mpoxopxnop0  7957  erdisj  8443  ixpprc  8600  sucdom2  8755  domunsn  8796  isinf  8891  nfielex  8903  enp1i  8909  xpfi  8942  scottex  9501  acndom  9665  axcclem  10071  axpowndlem3  10213  canthp1lem1  10266  isumltss  15412  pf1rcl  21265  ppttop  21904  ntreq0  21974  txindis  22531  txconn  22586  fmfnfm  22855  ptcmplem2  22950  ptcmplem3  22951  bddmulibl  24736  g0wlk0  27739  wwlksnndef  27989  strlem1  30331  disjorf  30637  ddemeas  31916  tgoldbachgt  32355  bnj1143  32483  prv1n  33106  pibt2  35325  poimirlem25  35539  poimirlem27  35541  ineleq  36223  eqvreldisj  36464  grucollcld  41551  fnchoice  42245  founiiun0  42401  nzerooringczr  45303  mo0sn  45834  map0cor  45855