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.) Avoid ax-11 2163, ax-12 2185. (Revised by GG, 28-Jun-2024.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2933  ∅c0 4287

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ne 2934  df-dif 3906  df-nul 4288

This theorem is referenced by:  reximdva0  4309  rspn0  4310  n0rex  4311  n0moeu  4313  eqeuel  4319  ndisj  4324  pssnel  4425  r19.2z  4454  r19.3rz  4456  uniintsn  4942  iunn0  5024  trintss  5225  intex  5291  notzfaus  5310  reusv2lem1  5345  nnullss  5417  exss  5418  opabn0  5509  wefrc  5626  wereu2  5629  dmxp  5886  xpnz  6125  dmsnn0  6173  unixp0  6249  xpco  6255  frpomin  6306  onfr  6364  iotanul2  6473  fveqdmss  7032  eldmrexrnb  7046  isofrlem  7296  limuni3  7804  soex  7873  f1oweALT  7926  fo1stres  7969  fo2ndres  7970  ecdmn0  8698  fsetprcnex  8811  map0g  8834  ixpn0  8880  resixpfo  8886  domdifsn  9000  xpdom3  9015  fodomr  9068  mapdom3  9089  0sdom1dom  9158  unblem2  9205  fodomfir  9240  marypha1lem  9348  brwdom2  9490  unxpwdom2  9505  ixpiunwdom  9507  zfreg  9513  epfrs  9652  frmin  9673  scott0  9810  cplem1  9813  fseqen  9949  finacn  9972  iunfictbso  10036  aceq2  10041  dfac3  10043  dfac9  10059  kmlem6  10078  kmlem8  10080  infpss  10138  fin23lem7  10238  enfin2i  10243  fin23lem21  10261  fin23lem31  10265  isf32lem9  10283  isf34lem4  10299  axdc2lem  10370  axdc3lem4  10375  ac6c4  10403  ac9  10405  ac6s4  10412  ac9s  10415  ttukeyg  10439  fpwwe2lem11  10564  wun0  10641  tsk0  10686  gruina  10741  genpn0  10926  prlem934  10956  ltaddpr  10957  ltexprlem1  10959  prlem936  10970  reclem2pr  10971  suplem1pr  10975  supsr  11035  axpre-sup  11092  dedekind  11308  dedekindle  11309  negn0  11578  infm3  12113  supaddc  12121  supadd  12122  supmul1  12123  supmullem2  12125  supmul  12126  zsupss  12862  xrsupsslem  13234  xrinfmsslem  13235  supxrre  13254  infxrre  13264  ixxub  13294  ixxlb  13295  ioorebas  13379  fzn0  13466  fzon0  13605  hashgt0elexb  14337  swrdcl  14581  pfxcl  14613  maxprmfct  16648  4sqlem12  16896  vdwmc  16918  ramz  16965  ramub1  16968  mreiincl  17527  mremre  17535  mreexexlem4d  17582  iscatd2  17616  catcone0  17622  cic  17735  drsdirfi  18240  mgmpropd  18588  opifismgm  18596  dfgrp3lem  18980  dfgrp3e  18982  issubg2  19083  subgint  19092  giclcl  19214  gicrcl  19215  gicsym  19216  gictr  19217  gicen  19219  gicsubgen  19220  cntzssv  19269  symggen  19411  psgnunilem3  19437  sylow1lem4  19542  odcau  19545  sylow3  19574  cyggex2  19838  giccyg  19841  pgpfac1lem5  20022  brric2  20451  subrngint  20505  subrgint  20540  abvn0b  20781  lss0cl  20910  lmiclcl  21034  lmicrcl  21035  lmicsym  21036  lspsnat  21112  lspprat  21120  cnsubrg  21394  nzerooringczr  21447  cygzn  21537  lmiclbs  21804  lmisfree  21809  lmictra  21812  mpfrcl  22052  ply1frcl  22274  mdetdiaglem  22554  mdet0  22562  toponmre  23049  iunconnlem  23383  iunconn  23384  unconn  23385  clsconn  23386  2ndcdisj  23412  2ndcsep  23415  1stcelcls  23417  locfincmp  23482  comppfsc  23488  txcls  23560  hmphsym  23738  hmphtr  23739  hmphen  23741  haushmphlem  23743  cmphmph  23744  connhmph  23745  reghmph  23749  nrmhmph  23750  hmphdis  23752  hmphen2  23755  fbdmn0  23790  isfbas2  23791  fbssint  23794  trfbas2  23799  filtop  23811  isfil2  23812  elfg  23827  fgcl  23834  filssufilg  23867  uffix2  23880  ufildom1  23882  hauspwpwf1  23943  hausflf2  23954  alexsubALTlem2  24004  ptcmplem2  24009  cnextf  24022  tgptsmscld  24107  ustfilxp  24169  xbln0  24370  lpbl  24459  met2ndci  24478  metustfbas  24513  restmetu  24526  reconn  24785  opnreen  24788  metdsre  24810  phtpcer  24962  phtpc01  24963  phtpcco2  24967  pcohtpy  24988  cfilfcls  25242  cmetcaulem  25256  cmetcau  25257  bcthlem5  25296  ovolicc2lem2  25487  ovolicc2lem5  25490  ioorcl2  25541  ioorinv2  25544  itg11  25660  dvlip  25966  dvne0  25984  fta1g  26143  plyssc  26173  fta1  26284  vieta1lem2  26287  nobdaymin  27761  sltstr  27795  ltslpss  27916  lrrecfr  27951  oncutlt  28272  hpgerlem  28849  axcontlem4  29052  axcontlem10  29058  upgrex  29177  fusgrn0degnn0  29585  uhgrvd00  29620  wspthsnonn0vne  30002  eulerpath  30328  frgrwopreglem2  30400  ubthlem1  30957  shintcli  31416  n0limd  32557  2ndimaxp  32735  fpwrelmapffslem  32821  qsxpid  33454  qsidomlem2  33545  qsdrng  33589  1arithidom  33629  dimcl  33779  lmimdim  33780  lmicdim  33781  lvecdim0i  33782  lvecdim0  33783  lssdimle  33784  dimpropd  33785  dimkerim  33804  fedgmul  33808  extdg1id  33843  fmcncfil  34108  insiga  34314  unelldsys  34335  bnj1189  35184  bnj1279  35193  axregszf  35304  pconnconn  35444  txsconn  35454  cvmsss2  35487  cvmopnlem  35491  cvmfolem  35492  cvmliftmolem2  35495  cvmlift2lem10  35525  cvmliftpht  35531  cvmlift3lem8  35539  eldm3  35974  fundmpss  35980  elima4  35989  neibastop1  36572  neibastop2lem  36573  neibastop2  36574  fnemeet2  36580  fnejoin2  36582  neifg  36584  tailfb  36590  filnetlem3  36593  bj-n0i  37193  bj-rest10  37335  bj-restn0  37337  poimirlem30  37895  itg2addnclem2  37917  prdsbnd2  38040  heibor1lem  38054  bfp  38069  divrngidl  38273  eldmres3  38528  rnxrn  38666  eldmxrncnvepres2  38680  trcoss2  38819  atex  39776  llnn0  39886  lplnn0N  39917  lvoln0N  39961  pmapglb2N  40141  pmapglb2xN  40142  elpaddn0  40170  osumcllem8N  40333  pexmidlem5N  40344  diaglbN  41425  diaintclN  41428  dibglbN  41536  dibintclN  41537  dihglblem2aN  41663  dihglblem5  41668  dihglbcpreN  41670  dihintcl  41714  unitscyglem5  42563  ricsym  42883  rictr  42884  riccrng1  42885  ricdrng1  42892  rencldnfilem  43171  kelac1  43414  lnmlmic  43439  gicabl  43450  neik0pk1imk0  44397  ntrneineine0lem  44433  scotteld  44596  onfrALT  44899  onfrALTVD  45240  iunconnlem2  45284  relpfrlem  45303  dfac5prim  45340  permac8prim  45364  snelmap  45436  eliin2f  45457  disjinfi  45545  mapss2  45557  difmap  45559  infrpge  45704  infxrlesupxr  45788  inficc  45888  fsumnncl  45926  ellimciota  45968  islpcn  45991  lptre2pt  45992  stoweidlem35  46387  fourierdlem31  46490  fourier2  46579  qndenserrnbllem  46646  qndenserrnopn  46650  qndenserrn  46651  intsaluni  46681  sge0cl  46733  ovn0lem  46917  ovnsubaddlem2  46923  hoidmvval0b  46942  hspdifhsp  46968  fsetprcnexALT  47416  uniimaelsetpreimafv  47750  imasetpreimafvbijlemfv1  47757  dfgric2  48269  gricuspgr  48272  gricsym  48275  grictr  48277  gricen  48279  dfgrlic2  48362  dfgrlic3  48364  grlicen  48371  gricgrlic  48372  usgrexmpl12ngric  48392  usgrexmpl12ngrlic  48393  opmpoismgm  48521  neircl  49258  sectrcl  49375  invrcl  49377  isorcl  49386  iinfssc  49410  iinfsubc  49411  imaid  49507  thincn0eu  49784  thinccic  49824  termcterm2  49867  eufunc  49875  euendfunc  49879  diag1f1o  49887  diag2f1o  49890  prstchom2ALT  49917  rellan  49976  relran  49977  alscn0d  50148