Theorem neq0 4276

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 2156, ax-12 2173. (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 1784	. . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
2		eq0 4274	. . 3 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
3	1, 2	xchbinxr 334	. 2 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ 𝐴 = ∅)
4	3	bicomi 223	1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-dif 3886  df-nul 4254

This theorem is referenced by:  n0  4277  ralidmOLD  4443  falseral0  4447  snprc  4650  pwpw0  4743  sssn  4756  pwsnOLD  4829  uni0b  4864  disjor  5050  rnep  5825  isomin  7188  mpoxneldm  7999  mpoxopynvov0g  8001  mpoxopxnop0  8002  erdisj  8508  ixpprc  8665  sucdom2  8822  domunsn  8863  isinf  8965  nfielex  8976  enp1i  8982  xpfi  9015  scottex  9574  acndom  9738  axcclem  10144  axpowndlem3  10286  canthp1lem1  10339  isumltss  15488  pf1rcl  21425  ppttop  22065  ntreq0  22136  txindis  22693  txconn  22748  fmfnfm  23017  ptcmplem2  23112  ptcmplem3  23113  bddmulibl  24908  g0wlk0  27921  wwlksnndef  28171  strlem1  30513  disjorf  30819  ddemeas  32104  tgoldbachgt  32543  bnj1143  32670  prv1n  33293  pibt2  35515  poimirlem25  35729  poimirlem27  35731  ineleq  36413  eqvreldisj  36654  grucollcld  41767  fnchoice  42461  founiiun0  42617  nzerooringczr  45518  mo0sn  46049  map0cor  46070