Theorem neq0 4073

Description: A nonempty class 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 2902	. 2 ⊢ Ⅎ𝑥𝐴
2	1	neq0f 4069	1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 196   = wceq 1632  ∃wex 1853   ∈ wcel 2139  ∅c0 4058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-dif 3718  df-nul 4059

This theorem is referenced by:  ralidm  4219  falseral0  4225  snprc  4397  pwpw0  4489  sssn  4503  pwsnALT  4581  uni0b  4615  disjor  4786  isomin  6750  mpt2xneldm  7507  mpt2xopynvov0g  7509  mpt2xopxnop0  7510  erdisj  7961  ixpprc  8095  domunsn  8275  sucdom2  8321  isinf  8338  nfielex  8354  enp1i  8360  xpfi  8396  scottex  8921  acndom  9064  axcclem  9471  axpowndlem3  9613  canthp1lem1  9666  isumltss  14779  pf1rcl  19915  ppttop  21013  ntreq0  21083  txindis  21639  txconn  21694  fmfnfm  21963  ptcmplem2  22058  ptcmplem3  22059  bddmulibl  23804  g0wlk0  26758  wwlksnndef  27023  strlem1  29418  disjorf  29699  ddemeas  30608  tgoldbachgt  31050  bnj1143  31168  poimirlem25  33747  poimirlem27  33749  ineleq  34442  fnchoice  39687  founiiun0  39876  nzerooringczr  42582