Theorem n0 3560

Description: A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 29-Sep-2006.)

Assertion

Ref	Expression
n0	⊢ (A ≠ ∅ ↔ ∃x x ∈ A)

Distinct variable group:   x,A

Proof of Theorem n0

Step	Hyp	Ref	Expression
1		nfcv 2490	. 2 ⊢ ℲxA
2	1	n0f 3559	1 ⊢ (A ≠ ∅ ↔ ∃x x ∈ A)

Syntax hints:   ↔ wb 176  ∃wex 1541   ∈ wcel 1710   ≠ wne 2517  ∅c0 3551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-dif 3216  df-nul 3552

This theorem is referenced by:  neq0  3561  reximdva0  3562  n0moeu  3563  pssnel  3616  r19.2z  3640  r19.2zb  3641  r19.3rz  3642  r19.3rzv  3644  uniintsn  3964  iunn0  4027  pw10b  4167  ndisjrelk  4324  prepeano4  4452  nnpw1ex  4485  tfindi  4497  tfinsuc  4499  sfinltfin  4536  vfintle  4547  nulnnn  4557  opabn0  4717  dmxp  4924  xpnz  5046  dmsnn0  5065  ecdmn0  5968  mapsspm  6022  mapsspw  6023  map0  6026  ncssfin  6152  ncspw1eu  6160  nntccl  6171  ce0nnul  6178  ce0nnulb  6183  fce  6189  lecidg  6197  lec0cg  6199  lecncvg  6200  addlec  6209  nc0le1  6217