Theorem n0 4277

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 2156, ax-12 2173. (Revised by Gino Giotto, 28-Jun-2024.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-ne 2943  df-dif 3886  df-nul 4254

This theorem is referenced by:  reximdva0  4282  rspn0  4283  rspn0OLD  4284  n0rex  4285  n0moeu  4287  eqeuel  4293  ndisj  4298  pssnel  4401  r19.2z  4422  r19.2zb  4423  r19.3rz  4424  uniintsn  4915  iunn0  4992  trintss  5204  intex  5256  notzfaus  5280  reusv2lem1  5316  nnullss  5371  exss  5372  opabn0  5459  wefrc  5574  wereu2  5577  dmxp  5827  xpnz  6051  dmsnn0  6099  unixp0  6175  xpco  6181  frpomin  6228  onfr  6290  fveqdmss  6938  eldmrexrnb  6950  isofrlem  7191  limuni3  7674  soex  7742  f1oweALT  7788  fo1stres  7830  fo2ndres  7831  ecdmn0  8503  fsetprcnex  8608  map0g  8630  ixpn0  8676  resixpfo  8682  domdifsn  8795  xpdom3  8810  fodomr  8864  mapdom3  8885  findcard2OLD  8986  unblem2  8997  marypha1lem  9122  brwdom2  9262  unxpwdom2  9277  ixpiunwdom  9279  zfreg  9284  epfrs  9420  frmin  9438  scott0  9575  cplem1  9578  fseqen  9714  finacn  9737  iunfictbso  9801  aceq2  9806  dfac3  9808  dfac9  9823  kmlem6  9842  kmlem8  9844  infpss  9904  fin23lem7  10003  enfin2i  10008  fin23lem21  10026  fin23lem31  10030  isf32lem9  10048  isf34lem4  10064  axdc2lem  10135  axdc3lem4  10140  ac6c4  10168  ac9  10170  ac6s4  10177  ac9s  10180  ttukeyg  10204  fpwwe2lem11  10328  wun0  10405  tsk0  10450  gruina  10505  genpn0  10690  prlem934  10720  ltaddpr  10721  ltexprlem1  10723  prlem936  10734  reclem2pr  10735  suplem1pr  10739  supsr  10799  axpre-sup  10856  dedekind  11068  dedekindle  11069  negn0  11334  infm3  11864  supaddc  11872  supadd  11873  supmul1  11874  supmullem2  11876  supmul  11877  zsupss  12606  xrsupsslem  12970  xrinfmsslem  12971  supxrre  12990  infxrre  12999  ixxub  13029  ixxlb  13030  ioorebas  13112  fzn0  13199  fzon0  13333  hashgt0elexb  14045  swrdcl  14286  pfxcl  14318  maxprmfct  16342  4sqlem12  16585  vdwmc  16607  ramz  16654  ramub1  16657  mreiincl  17222  mremre  17230  mreexexlem4d  17273  iscatd2  17307  catcone0  17313  cic  17428  drsdirfi  17938  opifismgm  18258  dfgrp3lem  18588  dfgrp3e  18590  issubg2  18685  subgint  18694  giclcl  18803  gicrcl  18804  gicsym  18805  gictr  18806  gicen  18808  gicsubgen  18809  cntzssv  18849  symggen  18993  psgnunilem3  19019  sylow1lem4  19121  odcau  19124  sylow3  19153  cyggex2  19413  giccyg  19416  pgpfac1lem5  19597  brric2  19904  subrgint  19961  lss0cl  20123  lmiclcl  20247  lmicrcl  20248  lmicsym  20249  lspsnat  20322  lspprat  20330  abvn0b  20486  cnsubrg  20570  cygzn  20690  lmiclbs  20954  lmisfree  20959  lmictra  20962  mpfrcl  21205  ply1frcl  21394  mdetdiaglem  21655  mdet0  21663  toponmre  22152  iunconnlem  22486  iunconn  22487  unconn  22488  clsconn  22489  2ndcdisj  22515  2ndcsep  22518  1stcelcls  22520  locfincmp  22585  comppfsc  22591  txcls  22663  hmphsym  22841  hmphtr  22842  hmphen  22844  haushmphlem  22846  cmphmph  22847  connhmph  22848  reghmph  22852  nrmhmph  22853  hmphdis  22855  hmphen2  22858  fbdmn0  22893  isfbas2  22894  fbssint  22897  trfbas2  22902  filtop  22914  isfil2  22915  elfg  22930  fgcl  22937  filssufilg  22970  uffix2  22983  ufildom1  22985  hauspwpwf1  23046  hausflf2  23057  alexsubALTlem2  23107  ptcmplem2  23112  cnextf  23125  tgptsmscld  23210  ustfilxp  23272  xbln0  23475  lpbl  23565  met2ndci  23584  metustfbas  23619  restmetu  23632  reconn  23897  opnreen  23900  metdsre  23922  phtpcer  24064  phtpc01  24065  phtpcco2  24068  pcohtpy  24089  cfilfcls  24343  cmetcaulem  24357  cmetcau  24358  bcthlem5  24397  ovolicc2lem2  24587  ovolicc2lem5  24590  ioorcl2  24641  ioorinv2  24644  itg11  24760  dvlip  25062  dvne0  25080  fta1g  25237  plyssc  25266  fta1  25373  vieta1lem2  25376  hpgerlem  27030  axcontlem4  27238  axcontlem10  27244  upgrex  27365  fusgrn0degnn0  27769  uhgrvd00  27804  wspthsnonn0vne  28183  eulerpath  28506  frgrwopreglem2  28578  ubthlem1  29133  shintcli  29592  2ndimaxp  30885  fpwrelmapffslem  30969  qsxpid  31460  qsidomlem2  31531  dimcl  31590  lvecdim0i  31591  lvecdim0  31592  lssdimle  31593  dimpropd  31594  dimkerim  31610  fedgmul  31614  extdg1id  31640  fmcncfil  31783  insiga  32005  unelldsys  32026  bnj521  32616  bnj1189  32889  bnj1279  32898  pconnconn  33093  txsconn  33103  cvmsss2  33136  cvmopnlem  33140  cvmfolem  33141  cvmliftmolem2  33144  cvmlift2lem10  33174  cvmliftpht  33180  cvmlift3lem8  33188  eldm3  33634  fundmpss  33646  elima4  33656  nocvxmin  33900  sslttr  33928  sltlpss  34014  lrrecfr  34027  neibastop1  34475  neibastop2lem  34476  neibastop2  34477  fnemeet2  34483  fnejoin2  34485  neifg  34487  tailfb  34493  filnetlem3  34496  bj-n0i  35067  bj-rest10  35186  bj-restn0  35188  poimirlem30  35734  itg2addnclem2  35756  prdsbnd2  35880  heibor1lem  35894  bfp  35909  divrngidl  36113  rnxrn  36451  trcoss2  36529  atex  37347  llnn0  37457  lplnn0N  37488  lvoln0N  37532  pmapglb2N  37712  pmapglb2xN  37713  elpaddn0  37741  osumcllem8N  37904  pexmidlem5N  37915  diaglbN  38996  diaintclN  38999  dibglbN  39107  dibintclN  39108  dihglblem2aN  39234  dihglblem5  39239  dihglbcpreN  39241  dihintcl  39285  sn-iotanul  40121  rencldnfilem  40558  kelac1  40804  lnmlmic  40829  gicabl  40840  neik0pk1imk0  41546  ntrneineine0lem  41582  scotteld  41753  onfrALT  42058  onfrALTVD  42400  iunconnlem2  42444  snelmap  42521  eliin2f  42543  disjinfi  42620  mapss2  42634  difmap  42636  infrpge  42780  infxrlesupxr  42866  inficc  42962  fsumnncl  43003  ellimciota  43045  islpcn  43070  lptre2pt  43071  stoweidlem35  43466  fourierdlem31  43569  fourier2  43658  qndenserrnbllem  43725  qndenserrnopn  43729  qndenserrn  43730  intsaluni  43758  sge0cl  43809  ovn0lem  43993  ovnsubaddlem2  43999  hoidmvval0b  44018  hspdifhsp  44044  fsetprcnexALT  44443  uniimaelsetpreimafv  44736  imasetpreimafvbijlemfv1  44743  mgmpropd  45217  opmpoismgm  45249  nzerooringczr  45518  neircl  46086  thincn0eu  46201  thinccic  46230  prstchom2ALT  46246  alscn0d  46385