Theorem neq0 4327

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 2157, ax-12 2177. (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 4325	. . 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 2108  ∅c0 4308

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 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-dif 3929  df-nul 4309

This theorem is referenced by:  n0  4328  falseral0  4491  snprc  4693  pwpw0  4789  sssn  4802  uni0b  4909  disjor  5101  rnep  5906  isomin  7330  mpoxneldm  8211  mpoxopynvov0g  8213  mpoxopxnop0  8214  erdisj  8773  ixpprc  8933  sucdom2OLD  9096  domunsn  9141  sucdom2  9217  isinf  9268  isinfOLD  9269  nfielex  9279  enp1iOLD  9286  xpfiOLD  9331  scottex  9899  acndom  10065  axcclem  10471  axpowndlem3  10613  canthp1lem1  10666  isumltss  15864  nzerooringczr  21441  pf1rcl  22287  ppttop  22945  ntreq0  23015  txindis  23572  txconn  23627  fmfnfm  23896  ptcmplem2  23991  ptcmplem3  23992  bddmulibl  25792  g0wlk0  29632  wwlksnndef  29887  strlem1  32231  disjorf  32560  ssdifidlprm  33473  1arithufdlem4  33562  ddemeas  34267  tgoldbachgt  34695  bnj1143  34821  prv1n  35453  pibt2  37435  poimirlem25  37669  poimirlem27  37671  ineleq  38372  eqvreldisj  38632  grucollcld  44284  relpmin  44977  fnchoice  45053  founiiun0  45214  mo0sn  48794  map0cor  48833  termchom  49373