Theorem n0 3559

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 =/= (/) <-> E.x x e. A)

Distinct variable group:   x,A

Proof of Theorem n0

Step	Hyp	Ref	Expression
1		nfcv 2489	. 2 |- F/_xA
2	1	n0f 3558	1 |- (A =/= (/) <-> E.x x e. A)

Syntax hints:   <-> wb 176  E.wex 1541   e. wcel 1710   =/= wne 2516  (/)c0 3550

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 2478  df-ne 2518  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-dif 3215  df-nul 3551

This theorem is referenced by:  neq0  3560  reximdva0  3561  n0moeu  3562  pssnel  3615  r19.2z  3639  r19.2zb  3640  r19.3rz  3641  r19.3rzv  3643  uniintsn  3963  iunn0  4026  pw10b  4166  ndisjrelk  4323  prepeano4  4451  nnpw1ex  4484  tfindi  4496  tfinsuc  4498  sfinltfin  4535  vfintle  4546  nulnnn  4556  opabn0  4716  dmxp  4923  xpnz  5045  dmsnn0  5064  ecdmn0  5967  mapsspm  6021  mapsspw  6022  map0  6025  ncssfin  6151  ncspw1eu  6159  nntccl  6170  ce0nnul  6177  ce0nnulb  6182  fce  6188  lecidg  6196  lec0cg  6198  lecncvg  6199  addlec  6208  nc0le1  6216