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

Theorem n0 4263
 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.) Avoid ax-11 2159, ax-12 2176. (Revised by Gino Giotto, 28-Jun-2024.)
Assertion
Ref Expression
n0 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem n0
StepHypRef Expression
1 df-ne 2991 . 2 (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
2 neq0 4262 . 2 𝐴 = ∅ ↔ ∃𝑥 𝑥𝐴)
31, 2bitri 278 1 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1538  ∃wex 1781   ∈ wcel 2112   ≠ wne 2990  ∅c0 4246 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ne 2991  df-dif 3887  df-nul 4247 This theorem is referenced by:  reximdva0  4268  rspn0  4269  rspn0OLD  4270  n0rex  4271  n0moeu  4273  eqeuel  4279  ndisj  4284  pssnel  4381  r19.2z  4401  r19.2zb  4402  r19.3rz  4403  uniintsn  4878  iunn0  4955  trintss  5156  intex  5207  notzfaus  5230  notzfausOLD  5231  reusv2lem1  5267  nnullss  5322  exss  5323  opabn0  5408  wefrc  5517  wereu2  5520  dmxp  5767  xpnz  5987  dmsnn0  6035  unixp0  6106  xpco  6112  onfr  6202  fveqdmss  6827  eldmrexrnb  6839  isofrlem  7076  limuni3  7551  soex  7612  f1oweALT  7659  fo1stres  7701  fo2ndres  7702  ecdmn0  8323  map0g  8435  ixpn0  8481  resixpfo  8487  domdifsn  8587  xpdom3  8602  fodomr  8656  mapdom3  8677  findcard2  8746  unblem2  8759  marypha1lem  8885  brwdom2  9025  unxpwdom2  9040  ixpiunwdom  9042  zfreg  9047  epfrs  9161  scott0  9303  cplem1  9306  fseqen  9442  finacn  9465  iunfictbso  9529  aceq2  9534  dfac3  9536  dfac9  9551  kmlem6  9570  kmlem8  9572  infpss  9632  fin23lem7  9731  enfin2i  9736  fin23lem21  9754  fin23lem31  9758  isf32lem9  9776  isf34lem4  9792  axdc2lem  9863  axdc3lem4  9868  ac6c4  9896  ac9  9898  ac6s4  9905  ac9s  9908  ttukeyg  9932  fpwwe2lem12  10056  wun0  10133  tsk0  10178  gruina  10233  genpn0  10418  prlem934  10448  ltaddpr  10449  ltexprlem1  10451  prlem936  10462  reclem2pr  10463  suplem1pr  10467  supsr  10527  axpre-sup  10584  dedekind  10796  dedekindle  10797  negn0  11062  infm3  11591  supaddc  11599  supadd  11600  supmul1  11601  supmullem2  11603  supmul  11604  zsupss  12329  xrsupsslem  12692  xrinfmsslem  12693  supxrre  12712  infxrre  12721  ixxub  12751  ixxlb  12752  ioorebas  12833  fzn0  12920  fzon0  13054  hashgt0elexb  13763  swrdcl  14002  pfxcl  14034  maxprmfct  16047  4sqlem12  16286  vdwmc  16308  ramz  16355  ramub1  16358  mreiincl  16863  mremre  16871  mreexexlem4d  16914  iscatd2  16948  cic  17065  drsdirfi  17544  opifismgm  17865  dfgrp3lem  18193  dfgrp3e  18195  issubg2  18290  subgint  18299  giclcl  18408  gicrcl  18409  gicsym  18410  gictr  18411  gicen  18413  gicsubgen  18414  cntzssv  18454  symggen  18594  psgnunilem3  18620  sylow1lem4  18722  odcau  18725  sylow3  18754  cyggex2  19014  giccyg  19017  pgpfac1lem5  19198  brric2  19497  subrgint  19554  lss0cl  19715  lmiclcl  19839  lmicrcl  19840  lmicsym  19841  lspsnat  19914  lspprat  19922  abvn0b  20072  cnsubrg  20155  cygzn  20266  lmiclbs  20530  lmisfree  20535  lmictra  20538  mpfrcl  20761  ply1frcl  20946  mdetdiaglem  21207  mdet0  21215  toponmre  21702  iunconnlem  22036  iunconn  22037  unconn  22038  clsconn  22039  2ndcdisj  22065  2ndcsep  22068  1stcelcls  22070  locfincmp  22135  comppfsc  22141  txcls  22213  hmphsym  22391  hmphtr  22392  hmphen  22394  haushmphlem  22396  cmphmph  22397  connhmph  22398  reghmph  22402  nrmhmph  22403  hmphdis  22405  hmphen2  22408  fbdmn0  22443  isfbas2  22444  fbssint  22447  trfbas2  22452  filtop  22464  isfil2  22465  elfg  22480  fgcl  22487  filssufilg  22520  uffix2  22533  ufildom1  22535  hauspwpwf1  22596  hausflf2  22607  alexsubALTlem2  22657  ptcmplem2  22662  cnextf  22675  tgptsmscld  22760  ustfilxp  22822  xbln0  23025  lpbl  23114  met2ndci  23133  metustfbas  23168  restmetu  23181  reconn  23437  opnreen  23440  metdsre  23462  phtpcer  23604  phtpc01  23605  phtpcco2  23608  pcohtpy  23629  cfilfcls  23882  cmetcaulem  23896  cmetcau  23897  bcthlem5  23936  ovolicc2lem2  24126  ovolicc2lem5  24129  ioorcl2  24180  ioorinv2  24183  itg11  24299  dvlip  24600  dvne0  24618  fta1g  24772  plyssc  24801  fta1  24908  vieta1lem2  24911  hpgerlem  26563  axcontlem4  26765  axcontlem10  26771  upgrex  26889  fusgrn0degnn0  27293  uhgrvd00  27328  wspthsnonn0vne  27707  eulerpath  28030  frgrwopreglem2  28102  ubthlem1  28657  shintcli  29116  2ndimaxp  30413  fpwrelmapffslem  30498  qsxpid  30982  qsidomlem2  31041  dimcl  31095  lvecdim0i  31096  lvecdim0  31097  lssdimle  31098  dimpropd  31099  dimkerim  31115  fedgmul  31119  extdg1id  31145  fmcncfil  31288  insiga  31510  unelldsys  31531  bnj521  32121  bnj1189  32395  bnj1279  32404  pconnconn  32592  txsconn  32602  cvmsss2  32635  cvmopnlem  32639  cvmfolem  32640  cvmliftmolem2  32643  cvmlift2lem10  32673  cvmliftpht  32679  cvmlift3lem8  32687  eldm3  33111  fundmpss  33123  elima4  33133  frpomin  33192  frmin  33198  nocvxmin  33362  sslttr  33382  neibastop1  33821  neibastop2lem  33822  neibastop2  33823  fnemeet2  33829  fnejoin2  33831  neifg  33833  tailfb  33839  filnetlem3  33842  bj-n0i  34387  bj-rest10  34504  bj-restn0  34506  poimirlem30  35086  itg2addnclem2  35108  prdsbnd2  35232  heibor1lem  35246  bfp  35261  divrngidl  35465  rnxrn  35805  trcoss2  35883  atex  36701  llnn0  36811  lplnn0N  36842  lvoln0N  36886  pmapglb2N  37066  pmapglb2xN  37067  elpaddn0  37095  osumcllem8N  37258  pexmidlem5N  37269  diaglbN  38350  diaintclN  38353  dibglbN  38461  dibintclN  38462  dihglblem2aN  38588  dihglblem5  38593  dihglbcpreN  38595  dihintcl  38639  rencldnfilem  39758  kelac1  40004  lnmlmic  40029  gicabl  40040  neik0pk1imk0  40747  ntrneineine0lem  40783  scotteld  40951  onfrALT  41252  onfrALTVD  41594  iunconnlem2  41638  snelmap  41715  eliin2f  41737  suprnmpt  41795  disjinfi  41817  mapss2  41831  difmap  41833  infrpge  41980  infxrlesupxr  42070  inficc  42168  fsumnncl  42210  ellimciota  42253  islpcn  42278  lptre2pt  42279  stoweidlem35  42674  fourierdlem31  42777  fourier2  42866  qndenserrnbllem  42933  qndenserrnopn  42937  qndenserrn  42938  intsaluni  42966  sge0cl  43017  ovn0lem  43201  ovnsubaddlem2  43207  hoidmvval0b  43226  hspdifhsp  43252  uniimaelsetpreimafv  43910  imasetpreimafvbijlemfv1  43917  mgmpropd  44392  opmpoismgm  44424  nzerooringczr  44693  alscn0d  45320
 Copyright terms: Public domain W3C validator