Theorem neq0 4305

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 2178. (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 4303	. . 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 2109  ∅c0 4286

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-dif 3908  df-nul 4287

This theorem is referenced by:  n0  4306  falseral0  4469  snprc  4671  pwpw0  4767  sssn  4780  uni0b  4887  disjor  5077  rnep  5873  isomin  7278  mpoxneldm  8152  mpoxopynvov0g  8154  mpoxopxnop0  8155  erdisj  8689  ixpprc  8853  domunsn  9051  sucdom2  9127  isinf  9165  isinfOLD  9166  nfielex  9176  enp1iOLD  9183  xpfiOLD  9228  scottex  9800  acndom  9964  axcclem  10370  axpowndlem3  10512  canthp1lem1  10565  isumltss  15773  nzerooringczr  21405  pf1rcl  22252  ppttop  22910  ntreq0  22980  txindis  23537  txconn  23592  fmfnfm  23861  ptcmplem2  23956  ptcmplem3  23957  bddmulibl  25756  g0wlk0  29614  wwlksnndef  29868  strlem1  32212  disjorf  32541  ssdifidlprm  33405  1arithufdlem4  33494  ddemeas  34202  tgoldbachgt  34630  bnj1143  34756  prv1n  35403  pibt2  37390  poimirlem25  37624  poimirlem27  37626  ineleq  38321  dmcnvep  38346  eqvreldisj  38590  grucollcld  44233  relpmin  44926  fnchoice  45007  founiiun0  45168  mo0sn  48801  map0cor  48840  termchom  49474