Theorem n0 4328

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ≠ wne 2932  ∅c0 4308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-ne 2933  df-dif 3929  df-nul 4309

This theorem is referenced by:  reximdva0  4330  rspn0  4331  n0rex  4332  n0moeu  4334  eqeuel  4340  ndisj  4345  pssnel  4446  r19.2z  4470  r19.2zb  4471  r19.3rz  4472  uniintsn  4961  iunn0  5043  trintss  5248  intex  5314  notzfaus  5333  reusv2lem1  5368  nnullss  5437  exss  5438  opabn0  5528  wefrc  5648  wereu2  5651  dmxp  5908  dmxpOLD  5909  xpnz  6148  dmsnn0  6196  unixp0  6272  xpco  6278  frpomin  6329  onfr  6391  iotanul2  6500  fveqdmss  7067  eldmrexrnb  7081  isofrlem  7332  limuni3  7845  soex  7915  f1oweALT  7969  fo1stres  8012  fo2ndres  8013  ecdmn0  8766  fsetprcnex  8874  map0g  8896  ixpn0  8942  resixpfo  8948  domdifsn  9066  xpdom3  9082  fodomr  9140  mapdom3  9161  0sdom1dom  9244  unblem2  9299  fodomfir  9338  marypha1lem  9443  brwdom2  9585  unxpwdom2  9600  ixpiunwdom  9602  zfreg  9607  epfrs  9743  frmin  9761  scott0  9898  cplem1  9901  fseqen  10039  finacn  10062  iunfictbso  10126  aceq2  10131  dfac3  10133  dfac9  10149  kmlem6  10168  kmlem8  10170  infpss  10228  fin23lem7  10328  enfin2i  10333  fin23lem21  10351  fin23lem31  10355  isf32lem9  10373  isf34lem4  10389  axdc2lem  10460  axdc3lem4  10465  ac6c4  10493  ac9  10495  ac6s4  10502  ac9s  10505  ttukeyg  10529  fpwwe2lem11  10653  wun0  10730  tsk0  10775  gruina  10830  genpn0  11015  prlem934  11045  ltaddpr  11046  ltexprlem1  11048  prlem936  11059  reclem2pr  11060  suplem1pr  11064  supsr  11124  axpre-sup  11181  dedekind  11396  dedekindle  11397  negn0  11664  infm3  12199  supaddc  12207  supadd  12208  supmul1  12209  supmullem2  12211  supmul  12212  zsupss  12951  xrsupsslem  13321  xrinfmsslem  13322  supxrre  13341  infxrre  13351  ixxub  13381  ixxlb  13382  ioorebas  13466  fzn0  13553  fzon0  13692  hashgt0elexb  14418  swrdcl  14661  pfxcl  14693  maxprmfct  16726  4sqlem12  16974  vdwmc  16996  ramz  17043  ramub1  17046  mreiincl  17606  mremre  17614  mreexexlem4d  17657  iscatd2  17691  catcone0  17697  cic  17810  drsdirfi  18315  mgmpropd  18627  opifismgm  18635  dfgrp3lem  19019  dfgrp3e  19021  issubg2  19122  subgint  19131  giclcl  19254  gicrcl  19255  gicsym  19256  gictr  19257  gicen  19259  gicsubgen  19260  cntzssv  19309  symggen  19449  psgnunilem3  19475  sylow1lem4  19580  odcau  19583  sylow3  19612  cyggex2  19876  giccyg  19879  pgpfac1lem5  20060  brric2  20464  subrngint  20518  subrgint  20553  abvn0b  20794  lss0cl  20902  lmiclcl  21026  lmicrcl  21027  lmicsym  21028  lspsnat  21104  lspprat  21112  cnsubrg  21393  nzerooringczr  21439  cygzn  21529  lmiclbs  21795  lmisfree  21800  lmictra  21803  mpfrcl  22041  ply1frcl  22254  mdetdiaglem  22534  mdet0  22542  toponmre  23029  iunconnlem  23363  iunconn  23364  unconn  23365  clsconn  23366  2ndcdisj  23392  2ndcsep  23395  1stcelcls  23397  locfincmp  23462  comppfsc  23468  txcls  23540  hmphsym  23718  hmphtr  23719  hmphen  23721  haushmphlem  23723  cmphmph  23724  connhmph  23725  reghmph  23729  nrmhmph  23730  hmphdis  23732  hmphen2  23735  fbdmn0  23770  isfbas2  23771  fbssint  23774  trfbas2  23779  filtop  23791  isfil2  23792  elfg  23807  fgcl  23814  filssufilg  23847  uffix2  23860  ufildom1  23862  hauspwpwf1  23923  hausflf2  23934  alexsubALTlem2  23984  ptcmplem2  23989  cnextf  24002  tgptsmscld  24087  ustfilxp  24149  xbln0  24351  lpbl  24440  met2ndci  24459  metustfbas  24494  restmetu  24507  reconn  24766  opnreen  24769  metdsre  24791  phtpcer  24943  phtpc01  24944  phtpcco2  24948  pcohtpy  24969  cfilfcls  25224  cmetcaulem  25238  cmetcau  25239  bcthlem5  25278  ovolicc2lem2  25469  ovolicc2lem5  25472  ioorcl2  25523  ioorinv2  25526  itg11  25642  dvlip  25948  dvne0  25966  fta1g  26125  plyssc  26155  fta1  26266  vieta1lem2  26269  nocvxmin  27740  sslttr  27769  sltlpss  27862  lrrecfr  27893  hpgerlem  28690  axcontlem4  28892  axcontlem10  28898  upgrex  29017  fusgrn0degnn0  29425  uhgrvd00  29460  wspthsnonn0vne  29845  eulerpath  30168  frgrwopreglem2  30240  ubthlem1  30797  shintcli  31256  n0limd  32399  2ndimaxp  32570  fpwrelmapffslem  32655  qsxpid  33323  qsidomlem2  33414  qsdrng  33458  1arithidom  33498  dimcl  33588  lmimdim  33589  lmicdim  33590  lvecdim0i  33591  lvecdim0  33592  lssdimle  33593  dimpropd  33594  dimkerim  33613  fedgmul  33617  extdg1id  33653  fmcncfil  33908  insiga  34114  unelldsys  34135  bnj1189  34986  bnj1279  34995  pconnconn  35199  txsconn  35209  cvmsss2  35242  cvmopnlem  35246  cvmfolem  35247  cvmliftmolem2  35250  cvmlift2lem10  35280  cvmliftpht  35286  cvmlift3lem8  35294  eldm3  35724  fundmpss  35730  elima4  35739  neibastop1  36323  neibastop2lem  36324  neibastop2  36325  fnemeet2  36331  fnejoin2  36333  neifg  36335  tailfb  36341  filnetlem3  36344  bj-n0i  36915  bj-rest10  37052  bj-restn0  37054  poimirlem30  37620  itg2addnclem2  37642  prdsbnd2  37765  heibor1lem  37779  bfp  37794  divrngidl  37998  rnxrn  38362  trcoss2  38448  atex  39371  llnn0  39481  lplnn0N  39512  lvoln0N  39556  pmapglb2N  39736  pmapglb2xN  39737  elpaddn0  39765  osumcllem8N  39928  pexmidlem5N  39939  diaglbN  41020  diaintclN  41023  dibglbN  41131  dibintclN  41132  dihglblem2aN  41258  dihglblem5  41263  dihglbcpreN  41265  dihintcl  41309  unitscyglem5  42158  ricsym  42489  rictr  42490  riccrng1  42491  ricdrng1  42498  rencldnfilem  42790  kelac1  43034  lnmlmic  43059  gicabl  43070  neik0pk1imk0  44018  ntrneineine0lem  44054  scotteld  44218  onfrALT  44522  onfrALTVD  44863  iunconnlem2  44907  relpfrlem  44926  dfac5prim  44963  snelmap  45054  eliin2f  45076  disjinfi  45164  mapss2  45177  difmap  45179  infrpge  45326  infxrlesupxr  45411  inficc  45511  fsumnncl  45549  ellimciota  45591  islpcn  45616  lptre2pt  45617  stoweidlem35  46012  fourierdlem31  46115  fourier2  46204  qndenserrnbllem  46271  qndenserrnopn  46275  qndenserrn  46276  intsaluni  46306  sge0cl  46358  ovn0lem  46542  ovnsubaddlem2  46548  hoidmvval0b  46567  hspdifhsp  46593  fsetprcnexALT  47039  uniimaelsetpreimafv  47358  imasetpreimafvbijlemfv1  47365  dfgric2  47876  gricuspgr  47879  gricsym  47882  grictr  47884  gricen  47886  dfgrlic2  47961  dfgrlic3  47963  grlicen  47970  gricgrlic  47971  usgrexmpl12ngric  47990  usgrexmpl12ngrlic  47991  opmpoismgm  48090  neircl  48827  iinfssc  48972  iinfsubc  48973  imaid  49042  thincn0eu  49265  thinccic  49305  termcterm2  49347  eufunc  49355  euendfunc  49359  diag1f1o  49367  diag2f1o  49370  prstchom2ALT  49389  rellan  49446  relran  49447  alscn0d  49607