Theorem n0 4305

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1559  ∃wex 1798   ∈ wcel 2141   ≠ wne 2956  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-ne 2957  df-dif 3907  df-nul 4286

This theorem is referenced by:  reximdva0  4307  rspn0  4308  n0rex  4309  n0moeu  4311  eqeuel  4317  ndisj  4322  pssnel  4424  r19.2z  4452  r19.3rz  4454  uniintsn  4942  iunn0  5023  trintss  5225  intex  5299  notzfaus  5319  reusv2lem1  5354  nnullss  5428  exss  5429  opabn0  5522  wefrc  5639  wereu2  5642  dmxp  5903  xpnz  6141  dmsnn0  6190  unixp0  6266  xpco  6272  frpomin  6323  onfr  6381  iotanul2  6490  fveqdmss  7055  eldmrexrnb  7069  isofrlem  7320  limuni3  7828  soex  7898  f1oweALT  7949  fo1stres  7992  fo2ndres  7993  ecdmn0  8726  fsetprcnex  8839  map0g  8862  ixpn0  8908  resixpfo  8914  domdifsn  9028  xpdom3  9043  fodomr  9096  mapdom3  9117  0sdom1dom  9186  unblem2  9233  fodomfir  9268  marypha1lem  9376  brwdom2  9518  unxpwdom2  9533  ixpiunwdom  9535  zfreg  9541  epfrs  9683  frmin  9704  scott0  9841  cplem1  9844  fseqen  9980  finacn  10003  iunfictbso  10067  aceq2  10072  dfac3  10074  dfac9  10090  kmlem6  10109  kmlem8  10111  infpss  10169  fin23lem7  10270  enfin2i  10275  fin23lem21  10293  fin23lem31  10297  isf32lem9  10315  isf34lem4  10331  axdc2lem  10402  axdc3lem4  10407  ac6c4  10435  ac9  10437  ac6s4  10444  ac9s  10447  ttukeyg  10471  fpwwe2lem11  10596  wun0  10673  tsk0  10718  gruina  10773  genpn0  10958  prlem934  10988  ltaddpr  10989  ltexprlem1  10991  prlem936  11002  reclem2pr  11003  suplem1pr  11007  supsr  11067  axpre-sup  11124  dedekind  11343  dedekindle  11344  negn0  11613  infm3  12148  supaddc  12156  supadd  12157  supmul1  12158  supmullem2  12160  supmul  12161  zsupss  12935  xrsupsslem  13307  xrinfmsslem  13308  supxrre  13327  infxrre  13337  ixxub  13367  ixxlb  13368  ioorebas  13452  fzn0  13540  fzon0  13680  hashgt0elexb  14412  swrdcl  14656  pfxcl  14688  maxprmfct  16727  4sqlem12  16975  vdwmc  16997  ramz  17044  ramub1  17047  mreiincl  17607  mremre  17615  mreexexlem4d  17662  iscatd2  17696  catcone0  17702  cic  17815  drsdirfi  18320  mgmpropd  18668  opifismgm  18676  dfgrp3lem  19063  dfgrp3e  19065  issubg2  19166  subgint  19175  giclcl  19296  gicrcl  19297  gicsym  19298  gictr  19299  gicen  19301  gicsubgen  19302  cntzssv  19351  symggen  19493  psgnunilem3  19519  sylow1lem4  19624  odcau  19627  sylow3  19656  cyggex2  19920  giccyg  19923  pgpfac1lem5  20104  ricsym  20534  brric2  20535  subrngint  20589  subrgint  20624  abvn0b  20865  lss0cl  20994  lmiclcl  21117  lmicrcl  21118  lmicsym  21119  lspsnat  21195  lspprat  21203  cnsubrg  21459  nzerooringczr  21512  cygzn  21602  lmiclbs  21869  lmisfree  21874  lmictra  21877  mpfrcl  22118  ply1frcl  22361  mdetdiaglem  22638  mdet0  22646  toponmre  23133  iunconnlem  23467  iunconn  23468  unconn  23469  clsconn  23470  2ndcdisj  23496  2ndcsep  23499  1stcelcls  23501  locfincmp  23566  comppfsc  23572  txcls  23644  hmphsym  23822  hmphtr  23823  hmphen  23825  haushmphlem  23827  cmphmph  23828  connhmph  23829  reghmph  23833  nrmhmph  23834  hmphdis  23836  hmphen2  23839  fbdmn0  23874  isfbas2  23875  fbssint  23878  trfbas2  23883  filtop  23895  isfil2  23896  elfg  23911  fgcl  23918  filssufilg  23951  uffix2  23964  ufildom1  23966  hauspwpwf1  24027  hausflf2  24038  alexsubALTlem2  24088  ptcmplem2  24093  cnextf  24106  tgptsmscld  24191  ustfilxp  24253  xbln0  24454  lpbl  24543  met2ndci  24562  metustfbas  24597  restmetu  24610  reconn  24869  opnreen  24872  metdsre  24894  phtpcer  25037  phtpc01  25038  phtpcco2  25041  pcohtpy  25062  cfilfcls  25316  cmetcaulem  25330  cmetcau  25331  bcthlem5  25370  ovolicc2lem2  25560  ovolicc2lem5  25563  ioorcl2  25614  ioorinv2  25617  itg11  25733  dvlip  26035  dvne0  26053  fta1g  26210  plyssc  26240  fta1  26349  vieta1lem2  26352  nobdaymin  27823  sltstr  27857  ltslpss  27978  lrrecfr  28013  oncutlt  28334  hpgerlem  28911  axcontlem4  29114  axcontlem10  29120  upgrex  29239  fusgrn0degnn0  29646  uhgrvd00  29681  wspthsnonn0vne  30063  eulerpath  30389  frgrwopreglem2  30461  ubthlem1  31019  shintcli  31478  n0limd  32619  2ndimaxp  32798  fpwrelmapffslem  32884  qsxpid  33509  qsidomlem2  33601  qsdrng  33646  1arithidom  33694  dimcl  33861  lmimdim  33862  lmicdim  33863  lvecdim0i  33864  lvecdim0  33865  lssdimle  33866  dimpropd  33867  dimkerim  33885  fedgmul  33889  extdg1id  33924  fmcncfil  34189  insiga  34395  unelldsys  34416  bnj1189  35268  bnj1279  35277  axregszf  35389  vonf1oonfo  35422  pconnconn  35545  txsconn  35555  cvmsss2  35588  cvmopnlem  35592  cvmfolem  35593  cvmliftmolem2  35596  cvmlift2lem10  35626  cvmliftpht  35632  cvmlift3lem8  35640  eldm3  36075  fundmpss  36081  elima4  36090  neibastop1  36683  neibastop2lem  36684  neibastop2  36685  fnemeet2  36691  fnejoin2  36693  neifg  36695  tailfb  36701  filnetlem3  36704  mh-infprim1bi  36870  bj-n0i  37400  bj-rest10  37542  bj-restn0  37544  poimirlem30  38113  itg2addnclem2  38135  prdsbnd2  38258  heibor1lem  38272  bfp  38287  divrngidl  38491  eldmres3  38746  rnxrn  38884  eldmxrncnvepres2  38898  trcoss2  39037  atex  39994  llnn0  40104  lplnn0N  40135  lvoln0N  40179  pmapglb2N  40359  pmapglb2xN  40360  elpaddn0  40388  osumcllem8N  40551  pexmidlem5N  40562  diaglbN  41643  diaintclN  41646  dibglbN  41754  dibintclN  41755  dihglblem2aN  41881  dihglblem5  41886  dihglbcpreN  41888  dihintcl  41932  unitscyglem5  42780  rictr  43102  riccrng1  43103  ricdrng1  43110  rencldnfilem  43361  kelac1  43604  lnmlmic  43629  gicabl  43640  neik0pk1imk0  44587  ntrneineine0lem  44623  scotteld  44786  onfrALT  45089  onfrALTVD  45430  iunconnlem2  45474  relpfrlem  45493  dfac5prim  45530  permac8prim  45554  snelmap  45626  eliin2f  45646  disjinfi  45734  mapss2  45746  difmap  45747  infrpge  45891  infxrlesupxr  45974  inficc  46074  fsumnncl  46112  ellimciota  46154  islpcn  46177  lptre2pt  46178  stoweidlem35  46573  fourierdlem31  46676  fourier2  46765  qndenserrnbllem  46832  qndenserrnopn  46836  qndenserrn  46837  intsaluni  46867  sge0cl  46919  ovn0lem  47103  ovnsubaddlem2  47109  hoidmvval0b  47128  hspdifhsp  47154  fsetprcnexALT  47620  uniimaelsetpreimafv  47966  imasetpreimafvbijlemfv1  47973  dfgric2  48501  gricuspgr  48504  gricsym  48507  grictr  48509  gricen  48511  dfgrlic2  48594  dfgrlic3  48596  grlicen  48603  gricgrlic  48604  usgrexmpl12ngric  48624  usgrexmpl12ngrlic  48625  opmpoismgm  48753  neircl  49490  sectrcl  49607  invrcl  49609  isorcl  49618  iinfssc  49642  iinfsubc  49643  imaid  49739  thincn0eu  50016  thinccic  50056  termcterm2  50099  eufunc  50107  euendfunc  50111  diag1f1o  50119  diag2f1o  50122  prstchom2ALT  50149  rellan  50208  relran  50209  alscn0d  50380