Theorem neq0 3930

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

Syntax hints:  ¬ wn 3   ↔ wb 196   = wceq 1483  ∃wex 1704   ∈ wcel 1990  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-nul 3916

This theorem is referenced by:  ralidm  4075  falseral0  4081  snprc  4253  pwpw0  4344  sssn  4358  pwsnALT  4429  uni0b  4463  disjor  4634  isomin  6587  mpt2xneldm  7338  mpt2xopynvov0g  7340  mpt2xopxnop0  7341  erdisj  7794  ixpprc  7929  domunsn  8110  sucdom2  8156  isinf  8173  nfielex  8189  enp1i  8195  xpfi  8231  scottex  8748  acndom  8874  axcclem  9279  axpowndlem3  9421  canthp1lem1  9474  isumltss  14580  pf1rcl  19713  ppttop  20811  ntreq0  20881  txindis  21437  txconn  21492  fmfnfm  21762  ptcmplem2  21857  ptcmplem3  21858  bddmulibl  23605  g0wlk0  26548  wwlksnndef  26800  clwwlksnndef  26890  strlem1  29109  disjorf  29392  ddemeas  30299  tgoldbachgt  30741  bnj1143  30861  poimirlem25  33434  poimirlem27  33436  ineleq  34119  fnchoice  39188  founiiun0  39377  nzerooringczr  42072