Theorem ne0 2292

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 973	. 2 |- (y e. A -> A.x y e. A)
2	1	ne0f 2291	1 |- (A =/= (/) <-> E.x x e. A)

Syntax hints:   <-> wb 146   e. wcel 960  E.wex 982   =/= wne 1588  (/)c0 2283

This theorem is referenced by:  n0 2293  abn0 2294  pssnel 2335  r19.2z 2351  r19.3rzv 2352  iunconst 2576  iunn0 2612  intex 2734  notzfaus 2746  nnullss 2774  exss 2775  opabn0 2830  wefrc 2949  onfr 2992  limuni3 3129  dmxp 3338  xpnz 3472  isofrlem 3907  f1oweALT 3912  iinon 3916  map0 4350  xpdom3 4451  fodomr 4489  0sdom1dom 4530  unblem2 4552  zfreg 4605  zfreg2 4606  zfregs 4657  scott0 4727  cplem1 4730  aceq2 4741  aceq3 4743  ac6s4 4771  ac9s 4774  kmlem6 4780  kmlem8 4782  genpn0 5118  prlem934 5151  ltaddpr 5152  ltexprlem1 5154  prlem936 5167  reclem1pr 5168  reclem2pr 5169  suplem1pr 5173  infm3 6056  infmrcl 6071  xrsupsslem 6078  xrinfmsslem 6079  supxrre 6085  acdc2 7491  acdc 7496  infpss 7575  iscms2lem5 7990  bcthlem8 8003  bcthlem14 8009  isgrp2i 8072  ubthlem6 8530  shintcl 9288  r19.3rzvb 10432  faimpex 10433  fine 10442

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2052  df-nul 2284

Copyright terms: Public domain