Theorem neq0 4301

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 2182. (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 4299	. . 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 4282

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 2705

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 2712  df-cleq 2725  df-dif 3901  df-nul 4283

This theorem is referenced by:  n0  4302  falseral0  4465  snprc  4669  pwpw0  4764  sssn  4777  uni0b  4884  disjor  5075  rnep  5871  isomin  7277  mpoxneldm  8148  mpoxopynvov0g  8150  mpoxopxnop0  8151  erdisj  8685  ixpprc  8849  domunsn  9047  sucdom2  9119  isinf  9156  nfielex  9165  scottex  9785  acndom  9949  axcclem  10355  axpowndlem3  10497  canthp1lem1  10550  isumltss  15757  nzerooringczr  21419  pf1rcl  22265  ppttop  22923  ntreq0  22993  txindis  23550  txconn  23605  fmfnfm  23874  ptcmplem2  23969  ptcmplem3  23970  bddmulibl  25768  g0wlk0  29631  wwlksnndef  29885  strlem1  32232  disjorf  32561  ssdifidlprm  33430  1arithufdlem4  33519  ddemeas  34270  tgoldbachgt  34697  bnj1143  34823  prv1n  35496  pibt2  37482  poimirlem25  37705  poimirlem27  37707  ineleq  38406  dmcnvep  38432  eqvreldisj  38730  grucollcld  44377  relpmin  45069  fnchoice  45150  founiiun0  45311  mo0sn  48940  map0cor  48979  termchom  49613