Theorem neq0 4190

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

Syntax hints:  ¬ wn 3   ↔ wb 198   = wceq 1507  ∃wex 1742   ∈ wcel 2048  ∅c0 4173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-dif 3828  df-nul 4174

This theorem is referenced by:  ralidm  4332  falseral0  4336  snprc  4521  pwpw0  4614  sssn  4627  pwsnALT  4699  uni0b  4731  disjor  4905  isomin  6907  mpoxneldm  7674  mpoxopynvov0g  7676  mpoxopxnop0  7677  erdisj  8133  ixpprc  8272  domunsn  8455  sucdom2  8501  isinf  8518  nfielex  8534  enp1i  8540  xpfi  8576  scottex  9100  acndom  9263  axcclem  9669  axpowndlem3  9811  canthp1lem1  9864  isumltss  15053  pf1rcl  20204  ppttop  21309  ntreq0  21379  txindis  21936  txconn  21991  fmfnfm  22260  ptcmplem2  22355  ptcmplem3  22356  bddmulibl  24132  g0wlk0  27126  wwlksnndef  27394  strlem1  29798  disjorf  30085  ddemeas  31097  tgoldbachgt  31543  bnj1143  31671  pibt2  34074  poimirlem25  34306  poimirlem27  34308  ineleq  35002  eqvreldisj  35242  grucollcld  39916  fnchoice  40649  founiiun0  40821  nzerooringczr  43647