Theorem neq0 4292

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 2153, ax-12 2170. (Revised by Gino Giotto, 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 4290	. . 3 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3	1, 2	xchbinxr 334	. 2 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ 𝐴 = ∅)
4	3	bicomi 223	1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1538   = wceq 1540  ∃wex 1780   ∈ wcel 2105  ∅c0 4269

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-dif 3901  df-nul 4270

This theorem is referenced by:  n0  4293  ralidmOLD  4460  falseral0  4464  snprc  4665  pwpw0  4760  sssn  4773  pwsnOLD  4845  uni0b  4881  disjor  5072  rnep  5868  isomin  7264  mpoxneldm  8098  mpoxopynvov0g  8100  mpoxopxnop0  8101  erdisj  8621  ixpprc  8778  sucdom2OLD  8947  domunsn  8992  sucdom2  9071  isinf  9125  isinfOLD  9126  nfielex  9138  enp1iOLD  9145  xpfiOLD  9183  scottex  9742  acndom  9908  axcclem  10314  axpowndlem3  10456  canthp1lem1  10509  isumltss  15659  pf1rcl  21621  ppttop  22263  ntreq0  22334  txindis  22891  txconn  22946  fmfnfm  23215  ptcmplem2  23310  ptcmplem3  23311  bddmulibl  25109  g0wlk0  28308  wwlksnndef  28558  strlem1  30900  disjorf  31205  ddemeas  32502  tgoldbachgt  32943  bnj1143  33069  prv1n  33692  pibt2  35693  poimirlem25  35907  poimirlem27  35909  ineleq  36620  eqvreldisj  36881  grucollcld  42199  fnchoice  42893  founiiun0  43055  nzerooringczr  45981  mo0sn  46512  map0cor  46533