Theorem n0 2286

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 1585	. 2 |- (A =/= (/) <-> -. A = (/))
2		ne0 2285	. 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 955   e. wcel 957  E.wex 979   =/= wne 1583  (/)c0 2277

This theorem is referenced by:  eq0 2291  ralidm 2354  snprc 2440  pwpw0 2466  sssn 2470  uni0b 2519  iununi 2612  unixp0 3514  isomin 3894  1st2val 4088  2nd2val 4089  ecdmn0 4273  mapdom2 4483  scottex 4699  axpowndlem3 4934  suplem1pr 5144  suppsrlem 5204  suppsr2 5206  suppsr3 5207  supsr 5214  suprelem 5242  fznt 6438  ntreq0 7668  strlem1 10133

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-v 1809  df-dif 2046  df-nul 2278

Copyright terms: Public domain