Theorem neq0 4299

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-dif 3902  df-nul 4280

This theorem is used by:  n0  4300  falseral0OLD  4471  snprc  4678  pwpw0  4774  sssn  4787  uni0b  4894  disjor  5085  rnep  5909  isomin  7337  mpoxneldm  8213  mpoxopynvov0g  8215  mpoxopxnop0  8216  erdisj  8759  ixpprc  8931  domunsn  9130  sucdom2  9202  isinf  9240  nfielex  9249  scottex  9914  scottexOLD  9915  acndom  10111  axcclem  10516  axpowndlem3  10665  canthp1lem1  10718  isumltss  15997  ssdifidlprm  21622  nzerooringczr  21766  pf1rcl  22647  ppttop  23305  ntreq0  23375  txindis  23933  txconn  23988  fmfnfm  24257  ptcmplem2  24352  ptcmplem3  24353  bddmulibl  26139  g0wlk0  30213  wwlksnndef  30476  strlem1  32834  disjorf  33155  1arithufdlem4  34061  ddemeas  34851  tgoldbachgt  35275  bnj1143  35403  rankscottu  35731  prv1n  36165  pibt2  38308  poimirlem25  38531  poimirlem27  38533  ineleq  39254  dmcnvep  39288  eqvreldisj  39598  grucollcld  45203  relpmin  45894  fnchoice  45989  founiiun0  46148  mo0sn  49870  map0cor  49909  termchom  50540