Theorem neq0 4302

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 2160, ax-12 2180. (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 4300	. . 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 2111  ∅c0 4283

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 2121  ax-ext 2703

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 2710  df-cleq 2723  df-dif 3905  df-nul 4284

This theorem is referenced by:  n0  4303  falseral0  4466  snprc  4670  pwpw0  4765  sssn  4778  uni0b  4885  disjor  5073  rnep  5867  isomin  7271  mpoxneldm  8142  mpoxopynvov0g  8144  mpoxopxnop0  8145  erdisj  8679  ixpprc  8843  domunsn  9040  sucdom2  9112  isinf  9149  nfielex  9158  scottex  9775  acndom  9939  axcclem  10345  axpowndlem3  10487  canthp1lem1  10540  isumltss  15752  nzerooringczr  21415  pf1rcl  22262  ppttop  22920  ntreq0  22990  txindis  23547  txconn  23602  fmfnfm  23871  ptcmplem2  23966  ptcmplem3  23967  bddmulibl  25765  g0wlk0  29627  wwlksnndef  29881  strlem1  32225  disjorf  32554  ssdifidlprm  33418  1arithufdlem4  33507  ddemeas  34244  tgoldbachgt  34671  bnj1143  34797  prv1n  35463  pibt2  37450  poimirlem25  37684  poimirlem27  37686  ineleq  38381  dmcnvep  38406  eqvreldisj  38650  grucollcld  44292  relpmin  44984  fnchoice  45065  founiiun0  45226  mo0sn  48846  map0cor  48885  termchom  49519