Theorem neq0 3889

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

Syntax hints:  ¬ wn 3   ↔ wb 195   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-nul 3875

This theorem is referenced by:  ralidm  4027  snprc  4197  pwpw0  4284  sssn  4298  pwsnALT  4367  uni0b  4399  disjor  4567  isomin  6487  mpt2xneldm  7225  mpt2xopynvov0g  7227  mpt2xopxnop0  7228  erdisj  7681  ixpprc  7815  domunsn  7995  sucdom2  8041  isinf  8058  nfielex  8074  enp1i  8080  xpfi  8116  scottex  8631  acndom  8757  axcclem  9162  axpowndlem3  9300  canthp1lem1  9353  isumltss  14419  pf1rcl  19534  ppttop  20621  ntreq0  20691  txindis  21247  txcon  21302  fmfnfm  21572  ptcmplem2  21667  ptcmplem3  21668  bddmulibl  23411  wwlknndef  26265  wlk0  26289  clwwlknndef  26301  strlem1  28493  disjorf  28774  ddemeas  29626  bnj1143  30115  poimirlem25  32604  poimirlem27  32606  fnchoice  38211  founiiun0  38372  falseral0  40308  g01wlk0  40860  wwlksnndef  41111  clwwlksnndef  41198  nzerooringczr  41864