Theorem n0 2289

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:   x,A

Proof of Theorem n0

Step	Hyp	Ref	Expression
1		df-ne 1587	. 2 |- (A =/= (/) <-> -. A = (/))
2		ne0 2288	. 2 |- (A =/= (/) <-> E.x x e. A)
3	1, 2	bitr3 175	1 |- (-. A = (/) <-> E.x x e. A)

Syntax hints:  -. wn 2   <-> wb 146   = wceq 956   e. wcel 958  E.wex 980   =/= wne 1585  (/)c0 2280

This theorem is referenced by:  eq0 2294  ralidm 2357  snprc 2443  pwpw0 2469  sssn 2473  pwsnALT 2501  uni0b 2523  iununi 2616  unixp0 3518  isomin 3899  1st2val 4095  2nd2val 4096  ecdmn0 4280  mapdom2 4494  scottex 4716  axpowndlem3 4951  suplem1pr 5161  suppsrlem 5221  suppsr2 5223  suppsr3 5224  supsr 5231  suprelem 5259  fznt 6493  ntreq0 7708  strlem1 10177

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-nul 2281

Copyright terms: Public domain