Theorem neq0 4309

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 2195, ax-12 2216. (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 4307	. . 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 2146  ∅c0 4289

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 2156  ax-ext 2738

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 2745  df-cleq 2758  df-dif 3911  df-nul 4290

This theorem is used by:  n0  4310  falseral0OLD  4481  snprc  4688  pwpw0  4784  sssn  4797  uni0b  4904  disjor  5096  rnep  5922  isomin  7346  mpoxneldm  8217  mpoxopynvov0g  8219  mpoxopxnop0  8220  erdisj  8761  ixpprc  8926  domunsn  9125  sucdom2  9197  isinf  9235  nfielex  9244  scottex  9872  scottexOLD  9873  acndom  10054  axcclem  10459  axpowndlem3  10602  canthp1lem1  10655  isumltss  15928  ssdifidlprm  21523  nzerooringczr  21667  pf1rcl  22546  ppttop  23201  ntreq0  23271  txindis  23828  txconn  23883  fmfnfm  24152  ptcmplem2  24247  ptcmplem3  24248  bddmulibl  26035  g0wlk0  30037  wwlksnndef  30291  strlem1  32639  disjorf  32961  1arithufdlem4  33868  ddemeas  34658  tgoldbachgt  35082  bnj1143  35210  rankscottu  35547  prv1n  35944  pibt2  38104  poimirlem25  38337  poimirlem27  38339  ineleq  39044  dmcnvep  39078  eqvreldisj  39388  grucollcld  45011  relpmin  45702  fnchoice  45790  founiiun0  45949  mo0sn  49635  map0cor  49674  termchom  50307