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

Theorem n0 3964
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 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem n0
StepHypRef Expression
1 nfcv 2793 . 2 𝑥𝐴
21n0f 3960 1 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wex 1744  wcel 2030  wne 2823  c0 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-v 3233  df-dif 3610  df-nul 3949
This theorem is referenced by:  reximdva0  3966  rspn0  3967  n0rex  3968  n0moeu  3970  eqeuel  3974  pssnel  4072  r19.2z  4093  r19.2zb  4094  r19.3rz  4095  uniintsn  4546  iunn0  4612  trintss  4802  intex  4850  notzfaus  4870  reusv2lem1  4898  nnullss  4960  exss  4961  opabn0  5035  wefrc  5137  wereu2  5140  dmxp  5376  xpnz  5588  dmsnn0  5635  unixp0  5707  xpco  5713  onfr  5801  fveqdmss  6394  eldmrexrnb  6406  isofrlem  6630  limuni3  7094  soex  7151  f1oweALT  7194  fo1stres  7236  fo2ndres  7237  ecdmn0  7832  map0g  7939  ixpn0  7982  resixpfo  7988  domdifsn  8084  xpdom3  8099  fodomr  8152  mapdom3  8173  findcard2  8241  unblem2  8254  marypha1lem  8380  brwdom2  8519  unxpwdom2  8534  ixpiunwdom  8537  zfreg  8541  epfrs  8645  scott0  8787  cplem1  8790  fseqen  8888  finacn  8911  iunfictbso  8975  aceq2  8980  dfac3  8982  dfac9  8996  kmlem6  9015  kmlem8  9017  infpss  9077  fin23lem7  9176  enfin2i  9181  fin23lem21  9199  fin23lem31  9203  isf32lem9  9221  isf34lem4  9237  axdc2lem  9308  axdc3lem4  9313  ac6c4  9341  ac9  9343  ac6s4  9350  ac9s  9353  ttukeyg  9377  fpwwe2lem12  9501  wun0  9578  tsk0  9623  gruina  9678  genpn0  9863  prlem934  9893  ltaddpr  9894  ltexprlem1  9896  prlem936  9907  reclem2pr  9908  suplem1pr  9912  supsr  9971  axpre-sup  10028  dedekind  10238  dedekindle  10239  negn0  10497  infm3  11020  supaddc  11028  supadd  11029  supmul1  11030  supmullem2  11032  supmul  11033  zsupss  11815  xrsupsslem  12175  xrinfmsslem  12176  supxrre  12195  infxrre  12204  ixxub  12234  ixxlb  12235  ioorebas  12313  fzn0  12393  fzon0  12526  hashgt0elexb  13228  swrdcl  13464  xpcogend  13759  maxprmfct  15468  4sqlem12  15707  vdwmc  15729  ramz  15776  ramub1  15779  mreiincl  16303  mremre  16311  mreexexlem4d  16354  iscatd2  16389  cic  16506  drsdirfi  16985  opifismgm  17305  dfgrp3lem  17560  dfgrp3e  17562  issubg2  17656  subgint  17665  giclcl  17761  gicrcl  17762  gicsym  17763  gictr  17764  gicen  17766  gicsubgen  17767  cntzssv  17807  symggen  17936  psgnunilem3  17962  sylow1lem4  18062  odcau  18065  sylow3  18094  cyggex2  18344  giccyg  18347  pgpfac1lem5  18524  brric2  18793  subrgint  18850  lss0cl  18995  lmiclcl  19118  lmicrcl  19119  lmicsym  19120  lspsnat  19193  lspprat  19201  abvn0b  19350  mpfrcl  19566  ply1frcl  19731  cnsubrg  19854  cygzn  19967  lmiclbs  20224  lmisfree  20229  lmictra  20232  mdetdiaglem  20452  mdet0  20460  toponmre  20945  iunconnlem  21278  iunconn  21279  unconn  21280  clsconn  21281  2ndcdisj  21307  2ndcsep  21310  1stcelcls  21312  locfincmp  21377  comppfsc  21383  txcls  21455  hmphsym  21633  hmphtr  21634  hmphen  21636  haushmphlem  21638  cmphmph  21639  connhmph  21640  reghmph  21644  nrmhmph  21645  hmphdis  21647  hmphen2  21650  fbdmn0  21685  isfbas2  21686  fbssint  21689  trfbas2  21694  filtop  21706  isfil2  21707  elfg  21722  fgcl  21729  filssufilg  21762  uffix2  21775  ufildom1  21777  hauspwpwf1  21838  hausflf2  21849  alexsubALTlem2  21899  ptcmplem2  21904  cnextf  21917  tgptsmscld  22001  ustfilxp  22063  xbln0  22266  lpbl  22355  met2ndci  22374  metustfbas  22409  restmetu  22422  reconn  22678  opnreen  22681  metdsre  22703  phtpcer  22841  phtpc01  22842  phtpcco2  22845  pcohtpy  22866  cfilfcls  23118  cmetcaulem  23132  cmetcau  23133  cmetss  23159  bcthlem5  23171  ovolicc2lem2  23332  ovolicc2lem5  23335  ioorcl2  23386  ioorinv2  23389  itg11  23503  dvlip  23801  dvne0  23819  fta1g  23972  plyssc  24001  fta1  24108  vieta1lem2  24111  hpgerlem  25702  axcontlem4  25892  axcontlem10  25898  upgrex  26032  fusgrn0degnn0  26451  uhgrvd00  26486  wspthsnonn0vne  26882  eulerpath  27219  frgrwopreglem2  27293  ubthlem1  27854  shintcli  28316  fpwrelmapffslem  29635  fmcncfil  30105  insiga  30328  unelldsys  30349  bnj521  30931  bnj1189  31203  bnj1279  31212  pconnconn  31339  txsconn  31349  cvmsss2  31382  cvmopnlem  31386  cvmfolem  31387  cvmliftmolem2  31390  cvmlift2lem10  31420  cvmliftpht  31426  cvmlift3lem8  31434  eldm3  31777  fundmpss  31790  elima4  31803  frpomin  31863  frmin  31867  nocvxmin  32019  sslttr  32039  neibastop1  32479  neibastop2lem  32480  neibastop2  32481  fnemeet2  32487  fnejoin2  32489  neifg  32491  tailfb  32497  filnetlem3  32500  bj-n0i  33060  bj-rest10  33166  bj-restn0  33168  poimirlem30  33569  itg2addnclem2  33592  prdsbnd2  33724  heibor1lem  33738  bfp  33753  divrngidl  33957  rnxrn  34296  trcoss2  34374  atex  35010  llnn0  35120  lplnn0N  35151  lvoln0N  35195  pmapglb2N  35375  pmapglb2xN  35376  elpaddn0  35404  osumcllem8N  35567  pexmidlem5N  35578  diaglbN  36661  diaintclN  36664  dibglbN  36772  dibintclN  36773  dihglblem2aN  36899  dihglblem5  36904  dihglbcpreN  36906  dihintcl  36950  rencldnfilem  37701  kelac1  37950  lnmlmic  37975  gicabl  37986  ndisj  38380  neik0pk1imk0  38662  ntrneineine0lem  38698  onfrALT  39081  onfrALTVD  39441  iunconnlem2  39485  snelmap  39568  eliin2f  39601  suprnmpt  39669  disjinfi  39694  mapss2  39711  difmap  39713  infrpge  39880  infxrlesupxr  39976  inficc  40079  fsumnncl  40121  ellimciota  40164  islpcn  40189  lptre2pt  40190  stoweidlem35  40570  fourierdlem31  40673  fourier2  40762  qndenserrnbllem  40832  qndenserrnopn  40836  qndenserrn  40837  intsaluni  40865  sge0cl  40916  ovn0lem  41100  ovnsubaddlem2  41106  hoidmvval0b  41125  hspdifhsp  41151  pfxcl  41711  mgmpropd  42100  opmpt2ismgm  42132  nzerooringczr  42397  alscn0d  42869
  Copyright terms: Public domain W3C validator