Theorem n0 4346

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 2154, ax-12 2171. (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 2941	. 2 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
2		neq0 4345	. 2 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
3	1, 2	bitri 274	1 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ≠ wne 2940  ∅c0 4322

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-ne 2941  df-dif 3951  df-nul 4323

This theorem is referenced by:  reximdva0  4351  rspn0  4352  rspn0OLD  4353  n0rex  4354  n0moeu  4356  eqeuel  4362  ndisj  4367  pssnel  4470  r19.2z  4494  r19.2zb  4495  r19.3rz  4496  uniintsn  4991  iunn0  5070  trintss  5284  intex  5337  notzfaus  5361  reusv2lem1  5396  nnullss  5462  exss  5463  opabn0  5553  wefrc  5670  wereu2  5673  dmxp  5928  xpnz  6158  dmsnn0  6206  unixp0  6282  xpco  6288  frpomin  6341  onfr  6403  iotanul2  6513  fveqdmss  7080  eldmrexrnb  7093  isofrlem  7339  limuni3  7843  soex  7914  f1oweALT  7961  fo1stres  8003  fo2ndres  8004  ecdmn0  8752  fsetprcnex  8858  map0g  8880  ixpn0  8926  resixpfo  8932  domdifsn  9056  xpdom3  9072  fodomr  9130  mapdom3  9151  0sdom1dom  9240  findcard2OLD  9286  unblem2  9298  marypha1lem  9430  brwdom2  9570  unxpwdom2  9585  ixpiunwdom  9587  zfreg  9592  epfrs  9728  frmin  9746  scott0  9883  cplem1  9886  fseqen  10024  finacn  10047  iunfictbso  10111  aceq2  10116  dfac3  10118  dfac9  10133  kmlem6  10152  kmlem8  10154  infpss  10214  fin23lem7  10313  enfin2i  10318  fin23lem21  10336  fin23lem31  10340  isf32lem9  10358  isf34lem4  10374  axdc2lem  10445  axdc3lem4  10450  ac6c4  10478  ac9  10480  ac6s4  10487  ac9s  10490  ttukeyg  10514  fpwwe2lem11  10638  wun0  10715  tsk0  10760  gruina  10815  genpn0  11000  prlem934  11030  ltaddpr  11031  ltexprlem1  11033  prlem936  11044  reclem2pr  11045  suplem1pr  11049  supsr  11109  axpre-sup  11166  dedekind  11379  dedekindle  11380  negn0  11645  infm3  12175  supaddc  12183  supadd  12184  supmul1  12185  supmullem2  12187  supmul  12188  zsupss  12923  xrsupsslem  13288  xrinfmsslem  13289  supxrre  13308  infxrre  13317  ixxub  13347  ixxlb  13348  ioorebas  13430  fzn0  13517  fzon0  13652  hashgt0elexb  14364  swrdcl  14597  pfxcl  14629  maxprmfct  16648  4sqlem12  16891  vdwmc  16913  ramz  16960  ramub1  16963  mreiincl  17542  mremre  17550  mreexexlem4d  17593  iscatd2  17627  catcone0  17633  cic  17748  drsdirfi  18260  opifismgm  18580  dfgrp3lem  18923  dfgrp3e  18925  issubg2  19023  subgint  19032  giclcl  19148  gicrcl  19149  gicsym  19150  gictr  19151  gicen  19153  gicsubgen  19154  cntzssv  19194  symggen  19340  psgnunilem3  19366  sylow1lem4  19471  odcau  19474  sylow3  19503  cyggex2  19767  giccyg  19770  pgpfac1lem5  19951  brric2  20289  subrgint  20346  lss0cl  20562  lmiclcl  20686  lmicrcl  20687  lmicsym  20688  lspsnat  20764  lspprat  20772  abvn0b  20926  cnsubrg  21011  cygzn  21132  lmiclbs  21398  lmisfree  21403  lmictra  21406  mpfrcl  21654  ply1frcl  21844  mdetdiaglem  22107  mdet0  22115  toponmre  22604  iunconnlem  22938  iunconn  22939  unconn  22940  clsconn  22941  2ndcdisj  22967  2ndcsep  22970  1stcelcls  22972  locfincmp  23037  comppfsc  23043  txcls  23115  hmphsym  23293  hmphtr  23294  hmphen  23296  haushmphlem  23298  cmphmph  23299  connhmph  23300  reghmph  23304  nrmhmph  23305  hmphdis  23307  hmphen2  23310  fbdmn0  23345  isfbas2  23346  fbssint  23349  trfbas2  23354  filtop  23366  isfil2  23367  elfg  23382  fgcl  23389  filssufilg  23422  uffix2  23435  ufildom1  23437  hauspwpwf1  23498  hausflf2  23509  alexsubALTlem2  23559  ptcmplem2  23564  cnextf  23577  tgptsmscld  23662  ustfilxp  23724  xbln0  23927  lpbl  24019  met2ndci  24038  metustfbas  24073  restmetu  24086  reconn  24351  opnreen  24354  metdsre  24376  phtpcer  24518  phtpc01  24519  phtpcco2  24522  pcohtpy  24543  cfilfcls  24798  cmetcaulem  24812  cmetcau  24813  bcthlem5  24852  ovolicc2lem2  25042  ovolicc2lem5  25045  ioorcl2  25096  ioorinv2  25099  itg11  25215  dvlip  25517  dvne0  25535  fta1g  25692  plyssc  25721  fta1  25828  vieta1lem2  25831  nocvxmin  27287  sslttr  27316  sltlpss  27409  lrrecfr  27436  hpgerlem  28054  axcontlem4  28263  axcontlem10  28269  upgrex  28390  fusgrn0degnn0  28794  uhgrvd00  28829  wspthsnonn0vne  29209  eulerpath  29532  frgrwopreglem2  29604  ubthlem1  30161  shintcli  30620  2ndimaxp  31910  fpwrelmapffslem  31995  qsxpid  32519  qsidomlem2  32617  qsdrng  32656  dimcl  32746  lmimdim  32747  lmicdim  32748  lvecdim0i  32749  lvecdim0  32750  lssdimle  32751  dimpropd  32752  dimkerim  32771  fedgmul  32775  extdg1id  32801  fmcncfil  32980  insiga  33204  unelldsys  33225  bnj1189  34089  bnj1279  34098  pconnconn  34291  txsconn  34301  cvmsss2  34334  cvmopnlem  34338  cvmfolem  34339  cvmliftmolem2  34342  cvmlift2lem10  34372  cvmliftpht  34378  cvmlift3lem8  34386  eldm3  34806  fundmpss  34813  elima4  34822  neibastop1  35336  neibastop2lem  35337  neibastop2  35338  fnemeet2  35344  fnejoin2  35346  neifg  35348  tailfb  35354  filnetlem3  35357  bj-n0i  35924  bj-rest10  36061  bj-restn0  36063  poimirlem30  36610  itg2addnclem2  36632  prdsbnd2  36755  heibor1lem  36769  bfp  36784  divrngidl  36988  rnxrn  37360  trcoss2  37446  atex  38369  llnn0  38479  lplnn0N  38510  lvoln0N  38554  pmapglb2N  38734  pmapglb2xN  38735  elpaddn0  38763  osumcllem8N  38926  pexmidlem5N  38937  diaglbN  40018  diaintclN  40021  dibglbN  40129  dibintclN  40130  dihglblem2aN  40256  dihglblem5  40261  dihglbcpreN  40263  dihintcl  40307  ricsym  41184  rictr  41185  riccrng1  41186  ricdrng1  41192  rencldnfilem  41646  kelac1  41893  lnmlmic  41918  gicabl  41929  neik0pk1imk0  42886  ntrneineine0lem  42922  scotteld  43093  onfrALT  43398  onfrALTVD  43740  iunconnlem2  43784  snelmap  43859  eliin2f  43881  disjinfi  43976  mapss2  43989  difmap  43991  infrpge  44146  infxrlesupxr  44231  inficc  44332  fsumnncl  44373  ellimciota  44415  islpcn  44440  lptre2pt  44441  stoweidlem35  44836  fourierdlem31  44939  fourier2  45028  qndenserrnbllem  45095  qndenserrnopn  45099  qndenserrn  45100  intsaluni  45130  sge0cl  45182  ovn0lem  45366  ovnsubaddlem2  45372  hoidmvval0b  45391  hspdifhsp  45417  fsetprcnexALT  45857  uniimaelsetpreimafv  46149  imasetpreimafvbijlemfv1  46156  mgmpropd  46630  opmpoismgm  46662  subrngint  46824  nzerooringczr  47055  neircl  47621  thincn0eu  47736  thinccic  47765  prstchom2ALT  47783  alscn0d  47926