Theorem ne0 2288

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

Assertion

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

Distinct variable group:   x,A

Proof of Theorem ne0

Step	Hyp	Ref	Expression
1		ax-17 971	. 2 |- (y e. A -> A.x y e. A)
2	1	ne0f 2287	1 |- (A =/= (/) <-> E.x x e. A)

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

This theorem is referenced by:  n0 2289  abn0 2290  pssnel 2331  r19.2z 2347  r19.3rzv 2348  iunconst 2572  iunn0 2607  intex 2729  notzfaus 2741  nnullss 2768  exss 2769  opabn0 2824  wefrc 2943  onfr 2986  limuni3 3123  dmxp 3332  xpnz 3466  isofrlem 3901  f1oweALT 3906  iinon 3910  map0 4344  xpdom3 4445  fodomr 4483  0sdom1dom 4525  unblem2 4541  zfreg 4596  zfreg2 4597  zfregs 4647  scott0 4717  cplem1 4720  aceq2 4731  aceq3 4733  ac6s4 4761  ac9s 4764  kmlem6 4770  kmlem8 4772  genpn0 5106  prlem934 5139  ltaddpr 5140  ltexprlem1 5142  prlem936 5155  reclem1pr 5156  reclem2pr 5157  suplem1pr 5161  infm3 6054  infmrcl 6069  xrsupsslem 6076  xrinfmsslem 6077  supxrre 6083  acdc2 7490  acdc 7495  infpss 7574  iscms2lem5 7993  bcthlem8 8006  bcthlem14 8012  isgrp2i 8076  ubthlem6 8534  shintcl 9293  r19.3rzvb 10437  faimpex 10438  fine 10449  fineOLD 10450

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