Theorem neq0 4346

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 2155, ax-12 2172. (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 1783	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
2		eq0 4344	. . 3 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3	1, 2	xchbinxr 335	. 2 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ 𝐴 = ∅)
4	3	bicomi 223	1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1540   = wceq 1542  ∃wex 1782   ∈ wcel 2107  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-dif 3952  df-nul 4324

This theorem is referenced by:  n0  4347  ralidmOLD  4516  falseral0  4520  snprc  4722  pwpw0  4817  sssn  4830  pwsnOLD  4902  uni0b  4938  disjor  5129  rnep  5927  isomin  7334  mpoxneldm  8197  mpoxopynvov0g  8199  mpoxopxnop0  8200  erdisj  8755  ixpprc  8913  sucdom2OLD  9082  domunsn  9127  sucdom2  9206  isinf  9260  isinfOLD  9261  nfielex  9273  enp1iOLD  9280  xpfiOLD  9318  scottex  9880  acndom  10046  axcclem  10452  axpowndlem3  10594  canthp1lem1  10647  isumltss  15794  pf1rcl  21868  ppttop  22510  ntreq0  22581  txindis  23138  txconn  23193  fmfnfm  23462  ptcmplem2  23557  ptcmplem3  23558  bddmulibl  25356  g0wlk0  28909  wwlksnndef  29159  strlem1  31503  disjorf  31810  ddemeas  33234  tgoldbachgt  33675  bnj1143  33801  prv1n  34422  pibt2  36298  poimirlem25  36513  poimirlem27  36515  ineleq  37223  eqvreldisj  37484  grucollcld  43019  fnchoice  43713  founiiun0  43888  nzerooringczr  46970  mo0sn  47500  map0cor  47521