Theorem neq0 4309

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.)

Assertion

Ref	Expression
neq0	⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Distinct variable group:   𝑥,𝐴

Proof of Theorem neq0

Step	Hyp	Ref	Expression
1		nfcv 2977	. 2 ⊢ Ⅎ𝑥𝐴
2	1	neq0f 4306	1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1537  ∃wex 1780   ∈ wcel 2114  ∅c0 4291

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-dif 3939  df-nul 4292

This theorem is referenced by:  ralidm  4455  falseral0  4459  snprc  4653  pwpw0  4746  sssn  4759  pwsnOLD  4831  uni0b  4864  disjor  5046  rnep  5797  isomin  7090  mpoxneldm  7878  mpoxopynvov0g  7880  mpoxopxnop0  7881  erdisj  8341  ixpprc  8483  domunsn  8667  sucdom2  8714  isinf  8731  nfielex  8747  enp1i  8753  xpfi  8789  scottex  9314  acndom  9477  axcclem  9879  axpowndlem3  10021  canthp1lem1  10074  isumltss  15203  pf1rcl  20512  ppttop  21615  ntreq0  21685  txindis  22242  txconn  22297  fmfnfm  22566  ptcmplem2  22661  ptcmplem3  22662  bddmulibl  24439  g0wlk0  27433  wwlksnndef  27683  strlem1  30027  disjorf  30329  ddemeas  31495  tgoldbachgt  31934  bnj1143  32062  prv1n  32678  pibt2  34701  poimirlem25  34932  poimirlem27  34934  ineleq  35623  eqvreldisj  35864  grucollcld  40616  fnchoice  41306  founiiun0  41471  nzerooringczr  44363