Theorem neq0 4304

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-dif 3904  df-nul 4286

This theorem is referenced by:  n0  4305  falseral0OLD  4468  snprc  4674  pwpw0  4769  sssn  4782  uni0b  4889  disjor  5080  rnep  5876  isomin  7283  mpoxneldm  8154  mpoxopynvov0g  8156  mpoxopxnop0  8157  erdisj  8692  ixpprc  8857  domunsn  9055  sucdom2  9127  isinf  9165  nfielex  9174  scottex  9797  acndom  9961  axcclem  10367  axpowndlem3  10510  canthp1lem1  10563  isumltss  15771  nzerooringczr  21435  pf1rcl  22293  ppttop  22951  ntreq0  23021  txindis  23578  txconn  23633  fmfnfm  23902  ptcmplem2  23997  ptcmplem3  23998  bddmulibl  25796  g0wlk0  29724  wwlksnndef  29978  strlem1  32325  disjorf  32654  ssdifidlprm  33539  1arithufdlem4  33628  ddemeas  34393  tgoldbachgt  34820  bnj1143  34946  prv1n  35625  pibt2  37618  poimirlem25  37842  poimirlem27  37844  ineleq  38543  dmcnvep  38569  eqvreldisj  38867  grucollcld  44497  relpmin  45189  fnchoice  45270  founiiun0  45430  mo0sn  49057  map0cor  49096  termchom  49729