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

Theorem n0 4307
Description: A class is nonempty if and only if it 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 2974 . 2 𝑥𝐴
21n0f 4304 1 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wex 1771  wcel 2105  wne 3013  c0 4288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-dif 3936  df-nul 4289
This theorem is referenced by:  reximdva0  4309  rspn0  4310  n0rex  4311  n0moeu  4313  eqeuel  4319  ndisj  4324  pssnel  4416  r19.2z  4436  r19.2zb  4437  r19.3rz  4438  uniintsn  4904  iunn0  4980  trintss  5180  intex  5231  notzfaus  5253  notzfausOLD  5254  reusv2lem1  5289  nnullss  5345  exss  5346  opabn0  5431  wefrc  5542  wereu2  5545  dmxp  5792  xpnz  6009  dmsnn0  6057  unixp0  6127  xpco  6133  onfr  6223  fveqdmss  6838  eldmrexrnb  6850  isofrlem  7082  limuni3  7556  soex  7615  f1oweALT  7662  fo1stres  7704  fo2ndres  7705  ecdmn0  8325  map0g  8437  ixpn0  8482  resixpfo  8488  domdifsn  8588  xpdom3  8603  fodomr  8656  mapdom3  8677  findcard2  8746  unblem2  8759  marypha1lem  8885  brwdom2  9025  unxpwdom2  9040  ixpiunwdom  9043  zfreg  9047  epfrs  9161  scott0  9303  cplem1  9306  fseqen  9441  finacn  9464  iunfictbso  9528  aceq2  9533  dfac3  9535  dfac9  9550  kmlem6  9569  kmlem8  9571  infpss  9627  fin23lem7  9726  enfin2i  9731  fin23lem21  9749  fin23lem31  9753  isf32lem9  9771  isf34lem4  9787  axdc2lem  9858  axdc3lem4  9863  ac6c4  9891  ac9  9893  ac6s4  9900  ac9s  9903  ttukeyg  9927  fpwwe2lem12  10051  wun0  10128  tsk0  10173  gruina  10228  genpn0  10413  prlem934  10443  ltaddpr  10444  ltexprlem1  10446  prlem936  10457  reclem2pr  10458  suplem1pr  10462  supsr  10522  axpre-sup  10579  dedekind  10791  dedekindle  10792  negn0  11057  infm3  11588  supaddc  11596  supadd  11597  supmul1  11598  supmullem2  11600  supmul  11601  zsupss  12325  xrsupsslem  12688  xrinfmsslem  12689  supxrre  12708  infxrre  12717  ixxub  12747  ixxlb  12748  ioorebas  12827  fzn0  12909  fzon0  13043  hashgt0elexb  13751  swrdcl  13995  pfxcl  14027  maxprmfct  16041  4sqlem12  16280  vdwmc  16302  ramz  16349  ramub1  16352  mreiincl  16855  mremre  16863  mreexexlem4d  16906  iscatd2  16940  cic  17057  drsdirfi  17536  opifismgm  17857  dfgrp3lem  18135  dfgrp3e  18137  issubg2  18232  subgint  18241  giclcl  18350  gicrcl  18351  gicsym  18352  gictr  18353  gicen  18355  gicsubgen  18356  cntzssv  18396  symggen  18527  psgnunilem3  18553  sylow1lem4  18655  odcau  18658  sylow3  18687  cyggex2  18946  giccyg  18949  pgpfac1lem5  19130  brric2  19429  subrgint  19486  lss0cl  19647  lmiclcl  19771  lmicrcl  19772  lmicsym  19773  lspsnat  19846  lspprat  19854  abvn0b  20003  mpfrcl  20226  ply1frcl  20409  cnsubrg  20533  cygzn  20645  lmiclbs  20909  lmisfree  20914  lmictra  20917  mdetdiaglem  21135  mdet0  21143  toponmre  21629  iunconnlem  21963  iunconn  21964  unconn  21965  clsconn  21966  2ndcdisj  21992  2ndcsep  21995  1stcelcls  21997  locfincmp  22062  comppfsc  22068  txcls  22140  hmphsym  22318  hmphtr  22319  hmphen  22321  haushmphlem  22323  cmphmph  22324  connhmph  22325  reghmph  22329  nrmhmph  22330  hmphdis  22332  hmphen2  22335  fbdmn0  22370  isfbas2  22371  fbssint  22374  trfbas2  22379  filtop  22391  isfil2  22392  elfg  22407  fgcl  22414  filssufilg  22447  uffix2  22460  ufildom1  22462  hauspwpwf1  22523  hausflf2  22534  alexsubALTlem2  22584  ptcmplem2  22589  cnextf  22602  tgptsmscld  22686  ustfilxp  22748  xbln0  22951  lpbl  23040  met2ndci  23059  metustfbas  23094  restmetu  23107  reconn  23363  opnreen  23366  metdsre  23388  phtpcer  23526  phtpc01  23527  phtpcco2  23530  pcohtpy  23551  cfilfcls  23804  cmetcaulem  23818  cmetcau  23819  bcthlem5  23858  ovolicc2lem2  24046  ovolicc2lem5  24049  ioorcl2  24100  ioorinv2  24103  itg11  24219  dvlip  24517  dvne0  24535  fta1g  24688  plyssc  24717  fta1  24824  vieta1lem2  24827  hpgerlem  26478  axcontlem4  26680  axcontlem10  26686  upgrex  26804  fusgrn0degnn0  27208  uhgrvd00  27243  wspthsnonn0vne  27623  eulerpath  27947  frgrwopreglem2  28019  ubthlem1  28574  shintcli  29033  fpwrelmapffslem  30394  qsxpid  30854  qsidomlem2  30883  dimcl  30902  lvecdim0i  30903  lvecdim0  30904  lssdimle  30905  dimpropd  30906  dimkerim  30922  fedgmul  30926  extdg1id  30952  fmcncfil  31073  insiga  31295  unelldsys  31316  bnj521  31906  bnj1189  32178  bnj1279  32187  pconnconn  32375  txsconn  32385  cvmsss2  32418  cvmopnlem  32422  cvmfolem  32423  cvmliftmolem2  32426  cvmlift2lem10  32456  cvmliftpht  32462  cvmlift3lem8  32470  eldm3  32894  fundmpss  32906  elima4  32916  frpomin  32975  frmin  32981  nocvxmin  33145  sslttr  33165  neibastop1  33604  neibastop2lem  33605  neibastop2  33606  fnemeet2  33612  fnejoin2  33614  neifg  33616  tailfb  33622  filnetlem3  33625  bj-n0i  34159  bj-rest10  34273  bj-restn0  34275  poimirlem30  34803  itg2addnclem2  34825  prdsbnd2  34954  heibor1lem  34968  bfp  34983  divrngidl  35187  rnxrn  35526  trcoss2  35604  atex  36422  llnn0  36532  lplnn0N  36563  lvoln0N  36607  pmapglb2N  36787  pmapglb2xN  36788  elpaddn0  36816  osumcllem8N  36979  pexmidlem5N  36990  diaglbN  38071  diaintclN  38074  dibglbN  38182  dibintclN  38183  dihglblem2aN  38309  dihglblem5  38314  dihglbcpreN  38316  dihintcl  38360  rencldnfilem  39295  kelac1  39541  lnmlmic  39566  gicabl  39577  neik0pk1imk0  40275  ntrneineine0lem  40311  scotteld  40459  onfrALT  40760  onfrALTVD  41102  iunconnlem2  41146  snelmap  41223  eliin2f  41247  suprnmpt  41306  disjinfi  41330  mapss2  41344  difmap  41346  infrpge  41495  infxrlesupxr  41586  inficc  41686  fsumnncl  41728  ellimciota  41771  islpcn  41796  lptre2pt  41797  stoweidlem35  42197  fourierdlem31  42300  fourier2  42389  qndenserrnbllem  42456  qndenserrnopn  42460  qndenserrn  42461  intsaluni  42489  sge0cl  42540  ovn0lem  42724  ovnsubaddlem2  42730  hoidmvval0b  42749  hspdifhsp  42775  uniimaelsetpreimafv  43433  imasetpreimafvbijlemfv1  43440  mgmpropd  43919  opmpoismgm  43951  nzerooringczr  44271  alscn0d  44824
  Copyright terms: Public domain W3C validator