Theorem neq0 4315

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 4313	. . 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 4296

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 2701

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 2708  df-cleq 2721  df-dif 3917  df-nul 4297

This theorem is referenced by:  n0  4316  falseral0  4479  snprc  4681  pwpw0  4777  sssn  4790  uni0b  4897  disjor  5089  rnep  5890  isomin  7312  mpoxneldm  8191  mpoxopynvov0g  8193  mpoxopxnop0  8194  erdisj  8728  ixpprc  8892  domunsn  9091  sucdom2  9167  isinf  9207  isinfOLD  9208  nfielex  9218  enp1iOLD  9225  xpfiOLD  9270  scottex  9838  acndom  10004  axcclem  10410  axpowndlem3  10552  canthp1lem1  10605  isumltss  15814  nzerooringczr  21390  pf1rcl  22236  ppttop  22894  ntreq0  22964  txindis  23521  txconn  23576  fmfnfm  23845  ptcmplem2  23940  ptcmplem3  23941  bddmulibl  25740  g0wlk0  29580  wwlksnndef  29835  strlem1  32179  disjorf  32508  ssdifidlprm  33429  1arithufdlem4  33518  ddemeas  34226  tgoldbachgt  34654  bnj1143  34780  prv1n  35418  pibt2  37405  poimirlem25  37639  poimirlem27  37641  ineleq  38336  dmcnvep  38361  eqvreldisj  38605  grucollcld  44249  relpmin  44942  fnchoice  45023  founiiun0  45184  mo0sn  48804  map0cor  48843  termchom  49477