Theorem neq0 3888

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 2750	. 2 ⊢ Ⅎ𝑥𝐴
2	1	neq0f 3884	1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 194   = wceq 1474  ∃wex 1694   ∈ wcel 1976  ∅c0 3873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-dif 3542  df-nul 3874

This theorem is referenced by:  ralidm  4026  snprc  4196  pwpw0  4283  sssn  4295  pwsnALT  4361  uni0b  4393  disjor  4561  isomin  6465  mpt2xneldm  7202  mpt2xopynvov0g  7204  mpt2xopxnop0  7205  erdisj  7658  ixpprc  7792  domunsn  7972  sucdom2  8018  isinf  8035  nfielex  8051  enp1i  8057  xpfi  8093  scottex  8608  acndom  8734  axcclem  9139  axpowndlem3  9277  canthp1lem1  9330  isumltss  14365  pf1rcl  19480  ppttop  20563  ntreq0  20633  txindis  21189  txcon  21244  fmfnfm  21514  ptcmplem2  21609  ptcmplem3  21610  bddmulibl  23328  wwlknndef  26031  wlk0  26055  clwwlknndef  26067  strlem1  28299  disjorf  28580  ddemeas  29432  bnj1143  29921  poimirlem25  32407  poimirlem27  32409  fnchoice  38014  founiiun0  38175  falseral0  40113  g01wlk0  40862  wwlksnndef  41113  clwwlksnndef  41200  nzerooringczr  41866