Theorem neq0 4375

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 1778	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
2		eq0 4373	. . 3 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3	1, 2	xchbinxr 335	. 2 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ 𝐴 = ∅)
4	3	bicomi 224	1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1535   = wceq 1537  ∃wex 1777   ∈ wcel 2108  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-dif 3979  df-nul 4353

This theorem is referenced by:  n0  4376  falseral0  4539  snprc  4742  pwpw0  4838  sssn  4851  uni0b  4957  disjor  5148  rnep  5951  isomin  7373  mpoxneldm  8253  mpoxopynvov0g  8255  mpoxopxnop0  8256  erdisj  8817  ixpprc  8977  sucdom2OLD  9148  domunsn  9193  sucdom2  9269  isinf  9323  isinfOLD  9324  nfielex  9335  enp1iOLD  9342  xpfiOLD  9387  scottex  9954  acndom  10120  axcclem  10526  axpowndlem3  10668  canthp1lem1  10721  isumltss  15896  nzerooringczr  21514  pf1rcl  22374  ppttop  23035  ntreq0  23106  txindis  23663  txconn  23718  fmfnfm  23987  ptcmplem2  24082  ptcmplem3  24083  bddmulibl  25894  g0wlk0  29688  wwlksnndef  29938  strlem1  32282  disjorf  32601  ssdifidlprm  33451  1arithufdlem4  33540  ddemeas  34200  tgoldbachgt  34640  bnj1143  34766  prv1n  35399  pibt2  37383  poimirlem25  37605  poimirlem27  37607  ineleq  38310  eqvreldisj  38570  grucollcld  44229  fnchoice  44929  founiiun0  45097  mo0sn  48547  map0cor  48568