MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  n0 Structured version   Unicode version

Theorem n0 3634
Description: A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 29-Sep-2006.)
Assertion
Ref Expression
n0  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
Distinct variable group:    x, A

Proof of Theorem n0
StepHypRef Expression
1 nfcv 2569 . 2  |-  F/_ x A
21n0f 3633 1  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   E.wex 1589    e. wcel 1755    =/= wne 2596   (/)c0 3625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-v 2964  df-dif 3319  df-nul 3626
This theorem is referenced by:  neq0  3635  reximdva0  3636  rspn0  3637  n0moeu  3638  pssnel  3732  r19.2z  3757  r19.2zb  3758  r19.3rz  3759  r19.3rzv  3761  uniintsn  4153  iunn0  4218  trint0  4390  intex  4436  notzfaus  4455  reusv2lem1  4481  reusv5OLD  4490  nnullss  4542  exss  4543  opabn0  4608  wefrc  4701  wereu2  4704  onfr  4745  dmxp  5045  xpnz  5245  dmsnn0  5292  unixp0  5359  xpco  5365  eldmrexrnb  5838  isofrlem  6018  limuni3  6452  soex  6510  f1oweALT  6550  fo1stres  6589  fo2ndres  6590  ecdmn0  7131  map0g  7240  ixpn0  7283  resixpfo  7289  domdifsn  7382  xpdom3  7397  fodomr  7450  mapdom3  7471  findcard2  7540  unblem2  7553  marypha1lem  7671  brwdom2  7776  unxpwdom2  7791  ixpiunwdom  7794  zfreg  7798  zfreg2  7799  epfrs  7939  scott0  8081  cplem1  8084  fseqen  8185  finacn  8208  iunfictbso  8272  aceq2  8277  dfac3  8279  dfac9  8293  kmlem6  8312  kmlem8  8314  infpss  8374  fin23lem7  8473  enfin2i  8478  fin23lem21  8496  fin23lem31  8500  isf32lem9  8518  isf34lem4  8534  axdc2lem  8605  axdc3lem4  8610  ac6c4  8638  ac9  8640  ac6s4  8647  ac9s  8650  ttukeyg  8674  fpwwe2lem12  8796  wun0  8873  tsk0  8918  gruina  8973  genpn0  9160  prlem934  9190  ltaddpr  9191  ltexprlem1  9193  prlem936  9204  reclem2pr  9205  suplem1pr  9209  supsr  9267  axpre-sup  9324  dedekind  9521  dedekindle  9522  infm3  10277  supmul1  10283  supmullem2  10285  supmul  10286  infmrcl  10297  negn0  10929  zsupss  10932  xrsupsslem  11257  xrinfmsslem  11258  supxrre  11278  infmxrre  11286  ixxub  11309  ixxlb  11310  ioorebas  11379  fzn0  11451  fzon0  11553  hashgt0elexb  12144  swrdcl  12299  maxprmfct  13782  4sqlem12  14000  vdwmc  14022  ramz  14069  ramub1  14072  mreiincl  14517  mremre  14525  mreexexlem4d  14568  iscatd2  14602  drsdirfi  15091  issubg2  15676  subgint  15685  giclcl  15780  gicrcl  15781  gicsym  15782  gictr  15783  gicen  15785  gicsubgen  15786  cntzssv  15826  symggen  15956  psgnunilem3  15982  sylow1lem4  16080  odcau  16083  sylow3  16112  cyggex2  16353  giccyg  16356  pgpfac1lem5  16554  subrgint  16811  lss0cl  16950  lmiclcl  17073  lmicrcl  17074  lmicsym  17075  lspsnat  17148  lspprat  17156  abvn0b  17296  cnsubrg  17717  cygzn  17845  lmiclbs  18108  lmisfree  18113  lmictra  18116  mdet1  18250  toponmre  18539  iunconlem  18873  iuncon  18874  uncon  18875  clscon  18876  2ndcdisj  18902  2ndcsep  18905  1stcelcls  18907  txcls  19019  hmphsym  19197  hmphtr  19198  hmphen  19200  haushmphlem  19202  cmphmph  19203  conhmph  19204  reghmph  19208  nrmhmph  19209  hmphdis  19211  hmphen2  19214  fbdmn0  19249  isfbas2  19250  fbssint  19253  trfbas2  19258  filtop  19270  isfil2  19271  elfg  19286  fgcl  19293  filssufilg  19326  uffix2  19339  ufildom1  19341  hauspwpwf1  19402  hausflf2  19413  alexsubALTlem2  19462  ptcmplem2  19467  cnextf  19480  tgptsmscld  19567  ustfilxp  19629  xbln0  19831  lpbl  19920  met2ndci  19939  metustfbasOLD  19982  metustfbas  19983  restmetu  20004  reconn  20247  opnreen  20250  metdsre  20271  phtpcer  20409  phtpc01  20410  phtpcco2  20413  pcohtpy  20434  cfilfcls  20627  cmetcaulem  20641  cmetcau  20642  cmetss  20667  bcthlem5  20681  ovolicc2lem2  20843  ovolicc2lem5  20846  ioorcl2  20894  ioorinv2  20897  itg11  21011  dvlip  21307  dvne0  21325  mpfrcl  21370  fta1g  21524  plyssc  21553  fta1  21659  vieta1lem2  21662  axcontlem4  23036  axcontlem10  23042  umgraex  23080  eupath  23425  isgrp2d  23545  ubthlem1  24094  shintcli  24555  fpwrelmapffslem  25857  fmcncfil  26215  insiga  26434  pconcon  26968  txscon  26978  cvmsss2  27011  cvmopnlem  27015  cvmfolem  27016  cvmliftmolem2  27019  cvmlift2lem10  27049  cvmliftpht  27055  cvmlift3lem8  27063  eldm3  27419  fundmpss  27424  elima4  27437  frmin  27550  nocvxmin  27679  supaddc  28261  supadd  28262  itg2addnclem2  28288  locfincmp  28420  comppfsc  28423  neibastop1  28424  neibastop2lem  28425  neibastop2  28426  fnemeet2  28432  fnejoin2  28434  neifg  28436  tailfb  28442  filnetlem3  28445  prdsbnd2  28538  heibor1lem  28552  bfp  28567  divrngidl  28672  rencldnfilem  29004  kelac1  29261  lnmlmic  29286  gicabl  29299  stoweidlem35  29676  wlk0  30138  2spontn0vne  30252  usgn0fidegnn0  30468  frgrawopreglem2  30484  alscn0d  30854  onfrALT  30958  onfrALTVD  31329  iunconlem2  31373  bnj521  31430  bnj1189  31702  bnj1279  31711  bj-n0i  32021  atex  32623  llnn0  32733  lplnn0N  32764  lvoln0N  32808  pmapglb2N  32988  pmapglb2xN  32989  elpaddn0  33017  osumcllem8N  33180  pexmidlem5N  33191  diaglbN  34273  diaintclN  34276  dibglbN  34384  dibintclN  34385  dihglblem2aN  34511  dihglblem5  34516  dihglbcpreN  34518  dihintcl  34562
  Copyright terms: Public domain W3C validator