Theorem n0 4348

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 2146, ax-12 2166. (Revised by GG, 28-Jun-2024.)

Assertion

Ref	Expression
n0	⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

Step	Hyp	Ref	Expression
1		df-ne 2930	. 2 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
2		neq0 4347	. 2 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
3	1, 2	bitri 274	1 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1533  ∃wex 1773   ∈ wcel 2098   ≠ wne 2929  ∅c0 4324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-ne 2930  df-dif 3949  df-nul 4325

This theorem is referenced by:  reximdva0  4353  rspn0  4354  rspn0OLD  4355  n0rex  4356  n0moeu  4358  eqeuel  4364  ndisj  4369  pssnel  4474  r19.2z  4498  r19.2zb  4499  r19.3rz  4500  uniintsn  4994  iunn0  5074  trintss  5288  intex  5343  notzfaus  5366  reusv2lem1  5401  nnullss  5467  exss  5468  opabn0  5558  wefrc  5675  wereu2  5678  dmxp  5934  xpnz  6169  dmsnn0  6217  unixp0  6293  xpco  6299  frpomin  6352  onfr  6414  iotanul2  6523  fveqdmss  7091  eldmrexrnb  7105  isofrlem  7351  limuni3  7861  soex  7933  f1oweALT  7985  fo1stres  8028  fo2ndres  8029  ecdmn0  8782  fsetprcnex  8890  map0g  8912  ixpn0  8958  resixpfo  8964  domdifsn  9091  xpdom3  9107  fodomr  9165  mapdom3  9186  0sdom1dom  9275  findcard2OLD  9321  unblem2  9333  marypha1lem  9472  brwdom2  9612  unxpwdom2  9627  ixpiunwdom  9629  zfreg  9634  epfrs  9770  frmin  9788  scott0  9925  cplem1  9928  fseqen  10066  finacn  10089  iunfictbso  10153  aceq2  10158  dfac3  10160  dfac9  10175  kmlem6  10194  kmlem8  10196  infpss  10256  fin23lem7  10355  enfin2i  10360  fin23lem21  10378  fin23lem31  10382  isf32lem9  10400  isf34lem4  10416  axdc2lem  10487  axdc3lem4  10492  ac6c4  10520  ac9  10522  ac6s4  10529  ac9s  10532  ttukeyg  10556  fpwwe2lem11  10680  wun0  10757  tsk0  10802  gruina  10857  genpn0  11042  prlem934  11072  ltaddpr  11073  ltexprlem1  11075  prlem936  11086  reclem2pr  11087  suplem1pr  11091  supsr  11151  axpre-sup  11208  dedekind  11423  dedekindle  11424  negn0  11689  infm3  12220  supaddc  12228  supadd  12229  supmul1  12230  supmullem2  12232  supmul  12233  zsupss  12968  xrsupsslem  13335  xrinfmsslem  13336  supxrre  13355  infxrre  13364  ixxub  13394  ixxlb  13395  ioorebas  13477  fzn0  13564  fzon0  13699  hashgt0elexb  14414  swrdcl  14648  pfxcl  14680  maxprmfct  16705  4sqlem12  16953  vdwmc  16975  ramz  17022  ramub1  17025  mreiincl  17604  mremre  17612  mreexexlem4d  17655  iscatd2  17689  catcone0  17695  cic  17810  drsdirfi  18325  mgmpropd  18639  opifismgm  18647  dfgrp3lem  19027  dfgrp3e  19029  issubg2  19130  subgint  19139  giclcl  19262  gicrcl  19263  gicsym  19264  gictr  19265  gicen  19267  gicsubgen  19268  cntzssv  19317  symggen  19463  psgnunilem3  19489  sylow1lem4  19594  odcau  19597  sylow3  19626  cyggex2  19890  giccyg  19893  pgpfac1lem5  20074  brric2  20483  subrngint  20537  subrgint  20574  lss0cl  20871  lmiclcl  20995  lmicrcl  20996  lmicsym  20997  lspsnat  21073  lspprat  21081  abvn0b  21308  cnsubrg  21416  nzerooringczr  21462  cygzn  21560  lmiclbs  21827  lmisfree  21832  lmictra  21835  mpfrcl  22092  ply1frcl  22301  mdetdiaglem  22583  mdet0  22591  toponmre  23080  iunconnlem  23414  iunconn  23415  unconn  23416  clsconn  23417  2ndcdisj  23443  2ndcsep  23446  1stcelcls  23448  locfincmp  23513  comppfsc  23519  txcls  23591  hmphsym  23769  hmphtr  23770  hmphen  23772  haushmphlem  23774  cmphmph  23775  connhmph  23776  reghmph  23780  nrmhmph  23781  hmphdis  23783  hmphen2  23786  fbdmn0  23821  isfbas2  23822  fbssint  23825  trfbas2  23830  filtop  23842  isfil2  23843  elfg  23858  fgcl  23865  filssufilg  23898  uffix2  23911  ufildom1  23913  hauspwpwf1  23974  hausflf2  23985  alexsubALTlem2  24035  ptcmplem2  24040  cnextf  24053  tgptsmscld  24138  ustfilxp  24200  xbln0  24403  lpbl  24495  met2ndci  24514  metustfbas  24549  restmetu  24562  reconn  24827  opnreen  24830  metdsre  24852  phtpcer  25004  phtpc01  25005  phtpcco2  25009  pcohtpy  25030  cfilfcls  25285  cmetcaulem  25299  cmetcau  25300  bcthlem5  25339  ovolicc2lem2  25530  ovolicc2lem5  25533  ioorcl2  25584  ioorinv2  25587  itg11  25703  dvlip  26009  dvne0  26027  fta1g  26189  plyssc  26219  fta1  26328  vieta1lem2  26331  nocvxmin  27800  sslttr  27829  sltlpss  27922  lrrecfr  27949  hpgerlem  28684  axcontlem4  28893  axcontlem10  28899  upgrex  29020  fusgrn0degnn0  29428  uhgrvd00  29463  wspthsnonn0vne  29843  eulerpath  30166  frgrwopreglem2  30238  ubthlem1  30795  shintcli  31254  2ndimaxp  32555  fpwrelmapffslem  32637  qsxpid  33214  qsidomlem2  33305  qsdrng  33349  1arithidom  33389  dimcl  33469  lmimdim  33470  lmicdim  33471  lvecdim0i  33472  lvecdim0  33473  lssdimle  33474  dimpropd  33475  dimkerim  33494  fedgmul  33498  extdg1id  33524  fmcncfil  33702  insiga  33926  unelldsys  33947  bnj1189  34810  bnj1279  34819  pconnconn  35011  txsconn  35021  cvmsss2  35054  cvmopnlem  35058  cvmfolem  35059  cvmliftmolem2  35062  cvmlift2lem10  35092  cvmliftpht  35098  cvmlift3lem8  35106  eldm3  35531  fundmpss  35538  elima4  35547  neibastop1  36019  neibastop2lem  36020  neibastop2  36021  fnemeet2  36027  fnejoin2  36029  neifg  36031  tailfb  36037  filnetlem3  36040  bj-n0i  36606  bj-rest10  36743  bj-restn0  36745  poimirlem30  37299  itg2addnclem2  37321  prdsbnd2  37444  heibor1lem  37458  bfp  37473  divrngidl  37677  rnxrn  38044  trcoss2  38130  atex  39053  llnn0  39163  lplnn0N  39194  lvoln0N  39238  pmapglb2N  39418  pmapglb2xN  39419  elpaddn0  39447  osumcllem8N  39610  pexmidlem5N  39621  diaglbN  40702  diaintclN  40705  dibglbN  40813  dibintclN  40814  dihglblem2aN  40940  dihglblem5  40945  dihglbcpreN  40947  dihintcl  40991  ricsym  41940  rictr  41941  riccrng1  41942  ricdrng1  41948  rencldnfilem  42414  kelac1  42661  lnmlmic  42686  gicabl  42697  neik0pk1imk0  43651  ntrneineine0lem  43687  scotteld  43857  onfrALT  44162  onfrALTVD  44504  iunconnlem2  44548  snelmap  44620  eliin2f  44642  disjinfi  44736  mapss2  44749  difmap  44751  infrpge  44903  infxrlesupxr  44988  inficc  45089  fsumnncl  45130  ellimciota  45172  islpcn  45197  lptre2pt  45198  stoweidlem35  45593  fourierdlem31  45696  fourier2  45785  qndenserrnbllem  45852  qndenserrnopn  45856  qndenserrn  45857  intsaluni  45887  sge0cl  45939  ovn0lem  46123  ovnsubaddlem2  46129  hoidmvval0b  46148  hspdifhsp  46174  fsetprcnexALT  46614  uniimaelsetpreimafv  46905  imasetpreimafvbijlemfv1  46912  dfgric2  47400  gricuspgr  47403  gricsym  47406  grictr  47408  gricen  47410  dfgrlic2  47435  dfgrlic3  47437  grlicen  47444  gricgrlic  47445  opmpoismgm  47481  neircl  48175  thincn0eu  48290  thinccic  48319  prstchom2ALT  48337  alscn0d  48480