Theorem n0 1714

Description: A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20.

Assertion

Ref	Expression
n0	|- (-. A = (/) <-> E.x x e. A)

Distinct variable group(s):   x,A

Proof of Theorem n0

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 |- (y e. A -> A.x y e. A)
2	1	n0f 1713	1 |- (-. A = (/) <-> E.x x e. A)

Syntax hints:  -. wn 1   <-> wb 127  E.wex 678   = wceq 1091   e. wcel 1092  (/)c0 1707

This theorem is referenced by:  abn0 1715  eq0 1719  pssnel 1752  r19.2z 1766  r19.3rzv 1767  ralidm 1774  snprc 1838  sssn 1852  nnullss 1880  exss 1881  pwpw0 1883  uni0b 1939  intex 1986  iunconst 2000  iunn0 2029  iununi 2037  wefrc 2195  onfr 2237  dmxp 2552  isomin 2937  isofrlem 2939  f1oweOLD 2944  iinon 2948  1st2val 3097  ecdmn0 3217  map0 3268  xpdom3 3347  mapdom2 3389  0sdom1dom 3420  unblem2 3432  zfreg 3447  zfreg2 3448  zfregs 3491  scottex 3541  scott0 3542  cplem1 3545  aceq2 3554  aceq3 3556  kmlem6 3585  kmlem13 3592  fodomb 3615  axpowndlem3 3745  genpn0 3900  prlem934 3933  ltaddpr 3934  ltexprlem1 3936  prlem936 3949  reclem1pr 3950  reclem2pr 3951  suplem1pr 3955  suppsrlem 4015  suppsr2 4017  suppsr3 4018  supsr 4025  suprelem 4053  shintcl 5294  strlem1 5691

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-nul 1708

metamath.org