Theorem neq0 4318

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0

Step	Hyp	Ref	Expression
1		df-ex 1780	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
2		eq0 4316	. . 3 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3	1, 2	xchbinxr 335	. 2 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ 𝐴 = ∅)
4	3	bicomi 224	1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∅c0 4299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-dif 3920  df-nul 4300

This theorem is referenced by:  n0  4319  falseral0  4482  snprc  4684  pwpw0  4780  sssn  4793  uni0b  4900  disjor  5092  rnep  5893  isomin  7315  mpoxneldm  8194  mpoxopynvov0g  8196  mpoxopxnop0  8197  erdisj  8731  ixpprc  8895  sucdom2OLD  9056  domunsn  9097  sucdom2  9173  isinf  9214  isinfOLD  9215  nfielex  9225  enp1iOLD  9232  xpfiOLD  9277  scottex  9845  acndom  10011  axcclem  10417  axpowndlem3  10559  canthp1lem1  10612  isumltss  15821  nzerooringczr  21397  pf1rcl  22243  ppttop  22901  ntreq0  22971  txindis  23528  txconn  23583  fmfnfm  23852  ptcmplem2  23947  ptcmplem3  23948  bddmulibl  25747  g0wlk0  29587  wwlksnndef  29842  strlem1  32186  disjorf  32515  ssdifidlprm  33436  1arithufdlem4  33525  ddemeas  34233  tgoldbachgt  34661  bnj1143  34787  prv1n  35425  pibt2  37412  poimirlem25  37646  poimirlem27  37648  ineleq  38343  dmcnvep  38368  eqvreldisj  38612  grucollcld  44256  relpmin  44949  fnchoice  45030  founiiun0  45191  mo0sn  48808  map0cor  48847  termchom  49481