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

Theorem n0 3890
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 2751 . 2 𝑥𝐴
21n0f 3886 1 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 195  wex 1695  wcel 1977  wne 2780  c0 3874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-v 3175  df-dif 3543  df-nul 3875
This theorem is referenced by:  reximdva0  3891  rspn0  3892  n0moeu  3893  pssnel  3991  r19.2z  4012  r19.2zb  4013  r19.3rz  4014  uniintsn  4449  iunn0  4516  trint0  4698  intex  4747  notzfaus  4766  reusv2lem1  4794  nnullss  4857  exss  4858  opabn0  4931  wefrc  5032  wereu2  5035  dmxp  5265  xpnz  5472  dmsnn0  5518  unixp0  5586  xpco  5592  onfr  5680  fveqdmss  6262  eldmrexrnb  6274  isofrlem  6490  limuni3  6944  soex  7002  f1oweALT  7043  fo1stres  7083  fo2ndres  7084  ecdmn0  7676  map0g  7783  ixpn0  7826  resixpfo  7832  domdifsn  7928  xpdom3  7943  fodomr  7996  mapdom3  8017  findcard2  8085  unblem2  8098  marypha1lem  8222  brwdom2  8361  unxpwdom2  8376  ixpiunwdom  8379  zfreg  8383  zfregOLD  8385  zfreg2OLD  8386  epfrs  8490  scott0  8632  cplem1  8635  fseqen  8733  finacn  8756  iunfictbso  8820  aceq2  8825  dfac3  8827  dfac9  8841  kmlem6  8860  kmlem8  8862  infpss  8922  fin23lem7  9021  enfin2i  9026  fin23lem21  9044  fin23lem31  9048  isf32lem9  9066  isf34lem4  9082  axdc2lem  9153  axdc3lem4  9158  ac6c4  9186  ac9  9188  ac6s4  9195  ac9s  9198  ttukeyg  9222  fpwwe2lem12  9342  wun0  9419  tsk0  9464  gruina  9519  genpn0  9704  prlem934  9734  ltaddpr  9735  ltexprlem1  9737  prlem936  9748  reclem2pr  9749  suplem1pr  9753  supsr  9812  axpre-sup  9869  dedekind  10079  dedekindle  10080  negn0  10338  infm3  10861  supaddc  10867  supadd  10868  supmul1  10869  supmullem2  10871  supmul  10872  zsupss  11653  xrsupsslem  12009  xrinfmsslem  12010  supxrre  12029  infxrre  12038  ixxub  12067  ixxlb  12068  ioorebas  12146  fzn0  12226  fzon0  12356  hashgt0elexb  13051  swrdcl  13271  xpcogend  13561  maxprmfct  15259  4sqlem12  15498  vdwmc  15520  ramz  15567  ramub1  15570  mreiincl  16079  mremre  16087  mreexexlem4d  16130  iscatd2  16165  cic  16282  drsdirfi  16761  opifismgm  17081  dfgrp3lem  17336  dfgrp3e  17338  issubg2  17432  subgint  17441  giclcl  17537  gicrcl  17538  gicsym  17539  gictr  17540  gicen  17543  gicsubgen  17544  cntzssv  17584  symggen  17713  psgnunilem3  17739  sylow1lem4  17839  odcau  17842  sylow3  17871  cyggex2  18121  giccyg  18124  pgpfac1lem5  18301  brric2  18568  subrgint  18625  lss0cl  18768  lmiclcl  18891  lmicrcl  18892  lmicsym  18893  lspsnat  18966  lspprat  18974  abvn0b  19123  mpfrcl  19339  ply1frcl  19504  cnsubrg  19625  cygzn  19738  lmiclbs  19995  lmisfree  20000  lmictra  20003  mdetdiaglem  20223  mdet0  20231  toponmre  20707  iunconlem  21040  iuncon  21041  uncon  21042  clscon  21043  2ndcdisj  21069  2ndcsep  21072  1stcelcls  21074  locfincmp  21139  comppfsc  21145  txcls  21217  hmphsym  21395  hmphtr  21396  hmphen  21398  haushmphlem  21400  cmphmph  21401  conhmph  21402  reghmph  21406  nrmhmph  21407  hmphdis  21409  hmphen2  21412  fbdmn0  21448  isfbas2  21449  fbssint  21452  trfbas2  21457  filtop  21469  isfil2  21470  elfg  21485  fgcl  21492  filssufilg  21525  uffix2  21538  ufildom1  21540  hauspwpwf1  21601  hausflf2  21612  alexsubALTlem2  21662  ptcmplem2  21667  cnextf  21680  tgptsmscld  21764  ustfilxp  21826  xbln0  22029  lpbl  22118  met2ndci  22137  metustfbas  22172  restmetu  22185  reconn  22439  opnreen  22442  metdsre  22464  phtpcer  22602  phtpcerOLD  22603  phtpc01  22604  phtpcco2  22607  pcohtpy  22628  cfilfcls  22880  cmetcaulem  22894  cmetcau  22895  cmetss  22921  bcthlem5  22933  ovolicc2lem2  23093  ovolicc2lem5  23096  ioorcl2  23146  ioorinv2  23149  itg11  23264  dvlip  23560  dvne0  23578  fta1g  23731  plyssc  23760  fta1  23867  vieta1lem2  23870  hpgerlem  25457  axcontlem4  25647  axcontlem10  25653  upgrex  25759  umgraex  25852  2spontn0vne  26414  eupath  26508  usgn0fidegnn0  26556  frgrawopreglem2  26572  ubthlem1  27110  shintcli  27572  fpwrelmapffslem  28895  fmcncfil  29305  insiga  29527  unelldsys  29548  bnj521  30059  bnj1189  30331  bnj1279  30340  pconcon  30467  txscon  30477  cvmsss2  30510  cvmopnlem  30514  cvmfolem  30515  cvmliftmolem2  30518  cvmlift2lem10  30548  cvmliftpht  30554  cvmlift3lem8  30562  eldm3  30905  fundmpss  30910  elima4  30924  frmin  30983  nocvxmin  31090  neibastop1  31524  neibastop2lem  31525  neibastop2  31526  fnemeet2  31532  fnejoin2  31534  neifg  31536  tailfb  31542  filnetlem3  31545  bj-n0i  32127  bj-rest10  32222  bj-restn0  32224  poimirlem30  32609  itg2addnclem2  32632  prdsbnd2  32764  heibor1lem  32778  bfp  32793  divrngidl  32997  atex  33710  llnn0  33820  lplnn0N  33851  lvoln0N  33895  pmapglb2N  34075  pmapglb2xN  34076  elpaddn0  34104  osumcllem8N  34267  pexmidlem5N  34278  diaglbN  35362  diaintclN  35365  dibglbN  35473  dibintclN  35474  dihglblem2aN  35600  dihglblem5  35605  dihglbcpreN  35607  dihintcl  35651  rencldnfilem  36402  kelac1  36651  lnmlmic  36676  gicabl  36687  ndisj  37083  neik0pk1imk0  37365  ntrneineine0lem  37401  onfrALT  37785  onfrALTVD  38149  iunconlem2  38193  snelmap  38280  eliin2f  38316  suprnmpt  38350  disjinfi  38375  mapss2  38392  difmap  38394  infrpge  38508  inficc  38608  fsumnncl  38638  ellimciota  38681  islpcn  38706  lptre2pt  38707  stoweidlem35  38928  fourierdlem31  39031  fourier2  39120  qndenserrnbllem  39190  qndenserrnopn  39194  qndenserrn  39195  intsaluni  39223  sge0cl  39274  ovn0lem  39455  ovnsubaddlem2  39461  hoidmvval0b  39480  hspdifhsp  39506  pfxcl  40249  n0rex  40310  fusgrn0degnn0  40714  uhgrvd00  40750  wspthsnonn0vne  41124  eulerpath  41409  frgrwopreglem2  41482  mgmpropd  41565  opmpt2ismgm  41597  nzerooringczr  41864  alscn0d  42350
  Copyright terms: Public domain W3C validator