Theorem n0 4308

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1570  ∃wex 1809   ∈ wcel 2143   ≠ wne 2958  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-ne 2959  df-dif 3909  df-nul 4288

This theorem is referenced by:  n0limd  4309  reximdva0  4311  rspn0  4312  n0rex  4313  n0moeu  4315  eqeuel  4321  ndisj  4326  pssnel  4432  r19.2z  4461  r19.3rz  4463  uniintsn  4951  iunn0  5032  trintss  5238  intex  5316  notsep  5336  reusv2lem1  5371  nnullss  5445  exss  5446  opabn0  5540  wefrc  5657  wereu2  5660  dmxp  5921  xpnz  6158  dmsnn0  6210  unixp0  6286  xpco  6292  frpomin  6343  onfr  6402  iotanul2  6511  fveqdmss  7075  eldmrexrnb  7089  isofrlem  7340  limuni3  7849  soex  7919  f1oweALT  7970  fo1stres  8013  fo2ndres  8014  ecdmn0  8748  fsetprcnex  8860  map0g  8883  ixpn0  8929  resixpfo  8935  domdifsn  9049  xpdom3  9064  fodomr  9117  mapdom3  9138  0sdom1dom  9207  unblem2  9254  fodomfir  9288  marypha1lem  9394  brwdom2  9536  unxpwdom2  9551  ixpiunwdom  9553  zfreg  9559  epfrs  9701  frmin  9722  scott0  9861  scotteld  9873  cplem1  9876  fseqen  10012  finacn  10035  iunfictbso  10099  aceq2  10104  dfac3  10106  dfac9  10121  kmlem6  10140  kmlem8  10142  infpss  10200  fin23lem7  10301  enfin2i  10306  fin23lem21  10324  fin23lem31  10328  isf32lem9  10346  isf34lem4  10362  axdc2lem  10433  axdc3lem4  10438  ac6c4  10466  ac9  10468  ac6s4  10475  ac9s  10478  ttukeyg  10502  fpwwe2lem11  10627  wun0  10704  tsk0  10749  gruina  10804  genpn0  10989  prlem934  11019  ltaddpr  11020  ltexprlem1  11022  prlem936  11033  reclem2pr  11034  suplem1pr  11038  supsr  11098  axpre-sup  11155  dedekind  11374  dedekindle  11375  negn0  11644  infm3  12175  supaddc  12183  supadd  12184  supmul1  12185  supmullem2  12187  supmul  12188  zsupss  12962  xrsupsslem  13334  xrinfmsslem  13335  supxrre  13354  infxrre  13364  ixxub  13394  ixxlb  13395  ioorebas  13479  fzn0  13567  fzon0  13708  hashgt0elexb  14440  swrdcl  14685  pfxcl  14717  maxprmfct  16769  4sqlem12  17017  vdwmc  17039  ramz  17086  ramub1  17089  mreiincl  17649  mremre  17657  mreexexlem4d  17704  iscatd2  17738  catcone0  17744  cic  17857  drsdirfi  18362  mgmpropd  18710  opifismgm  18718  dfgrp3lem  19105  dfgrp3e  19107  issubg2  19209  subgint  19218  qsxpid  19244  giclcl  19344  gicrcl  19345  gicsym  19346  gictr  19347  gicen  19349  gicsubgen  19350  cntzssv  19399  symggen  19541  psgnunilem3  19567  sylow1lem4  19672  odcau  19675  sylow3  19704  cyggex2  19968  giccyg  19971  pgpfac1lem5  20152  ricsym  20589  brric2  20590  subrngint  20646  subrgint  20681  abvn0b  20920  lss0cl  21049  lmiclcl  21172  lmicrcl  21173  lmicsym  21174  lspsnat  21250  lspprat  21258  lidlunin0  21342  qsidomlem2  21462  cnsubrg  21558  nzerooringczr  21611  cygzn  21701  lmiclbs  21968  lmisfree  21973  lmictra  21976  mpfrcl  22217  ply1frcl  22459  mdetdiaglem  22736  mdet0  22744  toponmre  23231  iunconnlem  23565  iunconn  23566  unconn  23567  clsconn  23568  2ndcdisj  23594  2ndcsep  23597  1stcelcls  23599  locfincmp  23664  comppfsc  23670  txcls  23742  hmphsym  23920  hmphtr  23921  hmphen  23923  haushmphlem  23925  cmphmph  23926  connhmph  23927  reghmph  23931  nrmhmph  23932  hmphdis  23934  hmphen2  23937  fbdmn0  23972  isfbas2  23973  fbssint  23976  trfbas2  23981  filtop  23993  isfil2  23994  elfg  24009  fgcl  24016  filssufilg  24049  uffix2  24062  ufildom1  24064  hauspwpwf1  24125  hausflf2  24136  alexsubALTlem2  24186  ptcmplem2  24191  cnextf  24204  tgptsmscld  24289  ustfilxp  24351  xbln0  24552  lpbl  24641  met2ndci  24660  metustfbas  24695  restmetu  24708  reconn  24967  opnreen  24970  metdsre  24992  phtpcer  25135  phtpc01  25136  phtpcco2  25139  pcohtpy  25160  cfilfcls  25414  cmetcaulem  25428  cmetcau  25429  bcthlem5  25468  ovolicc2lem2  25658  ovolicc2lem5  25661  ioorcl2  25712  ioorinv2  25715  itg11  25831  dvlip  26133  dvne0  26151  fta1g  26308  plyssc  26338  fta1  26450  vieta1lem2  26453  nobdaymin  27927  sltstr  27961  ltslpss  28082  lrrecfr  28117  oncutlt  28438  hpgerlem  29028  axcontlem4  29298  axcontlem10  29304  upgrex  29423  fusgrn0degnn0  29830  uhgrvd00  29865  wspthsnonn0vne  30247  eulerpath  30573  frgrwopreglem2  30645  ubthlem1  31203  shintcli  31662  2ndimaxp  32972  fpwrelmapffslem  33058  qsdrng  33760  1arithidom  33808  dimcl  33974  lmimdim  33975  lmicdim  33976  lvecdim0i  33977  lvecdim0  33978  lssdimle  33979  dimpropd  33980  dimkerim  33998  fedgmul  34002  extdg1id  34037  fmcncfil  34302  insiga  34508  unelldsys  34529  bnj1189  35378  bnj1279  35387  rankscott  35503  axregszf  35523  karddom  35555  kardsdom  35556  vonf1oonfo  35580  pconnconn  35704  txsconn  35714  cvmsss2  35747  cvmopnlem  35751  cvmfolem  35752  cvmliftmolem2  35755  cvmlift2lem10  35785  cvmliftpht  35791  cvmlift3lem8  35799  eldm3  36234  fundmpss  36240  elima4  36249  neibastop1  36851  neibastop2lem  36852  neibastop2  36853  fnemeet2  36859  fnejoin2  36861  neifg  36863  tailfb  36869  filnetlem3  36872  mh-infprim1bi  37038  bj-n0i  37568  bj-rest10  37711  bj-restn0  37713  poimirlem30  38282  itg2addnclem2  38304  prdsbnd2  38427  heibor1lem  38441  bfp  38456  divrngidl  38660  eldmres3  38913  rnxrn  39051  eldmxrncnvepres2  39065  trcoss2  39204  atex  40161  llnn0  40271  lplnn0N  40302  lvoln0N  40346  pmapglb2N  40526  pmapglb2xN  40527  elpaddn0  40555  osumcllem8N  40718  pexmidlem5N  40729  diaglbN  41810  diaintclN  41813  dibglbN  41921  dibintclN  41922  dihglblem2aN  42048  dihglblem5  42053  dihglbcpreN  42055  dihintcl  42099  unitscyglem5  42947  rictr  43271  riccrng1  43272  ricdrng1  43279  rencldnfilem  43530  kelac1  43773  lnmlmic  43798  gicabl  43809  neik0pk1imk0  44756  ntrneineine0lem  44792  onfrALT  45241  onfrALTVD  45582  iunconnlem2  45626  relpfrlem  45645  dfac5prim  45682  permac8prim  45706  snelmap  45785  eliin2f  45805  disjinfi  45893  mapss2  45905  difmap  45906  infrpge  46050  infxrlesupxr  46133  inficc  46233  fsumnncl  46271  ellimciota  46313  islpcn  46336  lptre2pt  46337  stoweidlem35  46732  fourierdlem31  46835  fourier2  46924  qndenserrnbllem  46991  qndenserrnopn  46995  qndenserrn  46996  intsaluni  47026  sge0cl  47078  ovn0lem  47262  ovnsubaddlem2  47268  hoidmvval0b  47287  hspdifhsp  47313  fsetprcnexALT  47782  uniimaelsetpreimafv  48128  imasetpreimafvbijlemfv1  48135  dfgric2  48663  gricuspgr  48666  gricsym  48669  grictr  48671  gricen  48673  dfgrlic2  48756  dfgrlic3  48758  grlicen  48765  gricgrlic  48766  usgrexmpl12ngric  48786  usgrexmpl12ngrlic  48787  opmpoismgm  48915  neircl  49666  sectrcl  49783  invrcl  49785  isorcl  49794  iinfssc  49818  iinfsubc  49819  imaid  49915  thincn0eu  50192  thinccic  50232  termcterm2  50275  eufunc  50283  euendfunc  50287  diag1f1o  50295  diag2f1o  50298  prstchom2ALT  50325  rellan  50384  relran  50385  alsralrex  50573