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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0

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

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wal 1557   = wceq 1559  ∃wex 1798   ∈ wcel 2141  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-dif 3907  df-nul 4286

This theorem is referenced by:  n0  4305  falseral0OLD  4468  snprc  4675  pwpw0  4770  sssn  4783  uni0b  4891  disjor  5081  rnep  5901  isomin  7317  mpoxneldm  8187  mpoxopynvov0g  8189  mpoxopxnop0  8190  erdisj  8731  ixpprc  8897  domunsn  9095  sucdom2  9167  isinf  9205  nfielex  9214  scottex  9840  acndom  10004  axcclem  10411  axpowndlem3  10554  canthp1lem1  10607  isumltss  15861  nzerooringczr  21512  pf1rcl  22392  ppttop  23047  ntreq0  23117  txindis  23674  txconn  23729  fmfnfm  23998  ptcmplem2  24093  ptcmplem3  24094  bddmulibl  25881  g0wlk0  29797  wwlksnndef  30051  strlem1  32399  disjorf  32728  ssdifidlprm  33606  1arithufdlem4  33704  ddemeas  34494  tgoldbachgt  34921  bnj1143  35049  prv1n  35745  pibt2  37875  poimirlem25  38108  poimirlem27  38110  ineleq  38817  dmcnvep  38851  eqvreldisj  39161  grucollcld  44800  relpmin  45492  fnchoice  45573  founiiun0  45732  mo0sn  49401  map0cor  49440  termchom  50073