Theorem n0 4299

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1569  ∃wex 1811   ∈ wcel 2144   ≠ wne 2955  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-ne 2956  df-dif 4047  df-nul 4279

This theorem is used by:  n0limd  4300  reximdva0  4302  rspn0  4303  n0rex  4304  n0moeu  4306  eqeuel  4312  ndisj  4317  pssnel  4423  r19.2z  4454  r19.3rz  4456  uniintsn  4944  iunn0  5024  trintss  5230  intex  5304  notsep  5324  reusv2lem1  5359  nnullss  5429  exss  5430  opabn0  5527  wefrc  5644  wereu2  5647  dmxp  5910  xpnz  6149  dmsnn0  6208  unixp0  6286  xpco  6292  frpomin  6343  onfr  6402  iotanul2  6511  fveqdmss  7079  eldmrexrnb  7093  isofrlem  7349  limuni3  7864  soex  7934  f1oweALT  7985  fo1stres  8028  fo2ndres  8029  ecdmn0  8774  fsetprcnex  8888  map0g  8916  ixpn0  8962  resixpfo  8968  domdifsn  9083  xpdom3  9098  fodomr  9151  mapdom3  9172  0sdom1dom  9241  unblem2  9289  fodomfir  9323  marypha1lem  9429  brwdom2  9571  unxpwdom2  9586  ixpiunwdom  9588  zfreg  9594  epfrs  9736  frmin  9757  scott0b  9941  scott0OLD  9942  scotteld  9951  cplem1  9954  cplem1OLD  9955  karden  9963  fseqen  10110  finacn  10133  iunfictbso  10197  aceq2  10202  dfac3  10204  dfac9  10219  kmlem6  10238  kmlem8  10240  infpss  10298  fin23lem7  10398  enfin2i  10403  fin23lem21  10421  fin23lem31  10425  isf32lem9  10443  isf34lem4  10459  axdc2lem  10530  axdc3lem4  10535  ac6c4  10563  ac9  10565  ac6s4  10572  ac9s  10575  ttukeyg  10599  fpwwe2lem11  10730  wun0  10807  tsk0  10852  gruina  10907  genpn0  11092  prlem934  11122  ltaddpr  11123  ltexprlem1  11125  prlem936  11136  reclem2pr  11137  suplem1pr  11141  supsr  11201  axpre-sup  11258  dedekind  11477  dedekindle  11478  negn0  11749  infm3  12280  supaddc  12288  supadd  12289  supmul1  12290  supmullem2  12292  supmul  12293  zsupss  13068  xrsupsslem  13441  xrinfmsslem  13442  supxrre  13461  infxrre  13471  ixxub  13501  ixxlb  13502  ioorebas  13586  fzn0  13675  fzon0  13816  hashgt0elexb  14550  swrdcl  14798  pfxcl  14832  maxprmfct  16891  4sqlem12  17140  vdwmc  17162  ramz  17209  ramub1  17212  mreiincl  17772  mremre  17780  mreexexlem4d  17827  iscatd2  17861  catcone0  17867  cic  17980  drsdirfi  18485  mgmpropd  18835  opifismgm  18843  dfgrp3lem  19254  dfgrp3e  19256  issubg2  19358  subgint  19367  qsxpid  19393  giclcl  19493  gicrcl  19494  gicsym  19495  gictr  19496  gicen  19498  gicsubgen  19499  cntzssv  19548  symggen  19690  psgnunilem3  19716  sylow1lem4  19821  odcau  19824  sylow3  19853  cyggex2  20117  giccyg  20120  pgpfac1lem5  20301  riclcl  20755  ricrcl  20756  ricsym  20757  rictr  20758  isbrric2  20759  subrngint  20818  subrgint  20853  abvn0b  21099  lss0cl  21228  lmiclcl  21351  lmicrcl  21352  lmicsym  21353  lspsnat  21429  lspprat  21437  lidlunin0  21521  qsidomlem2  21643  cnsubrg  21739  nzerooringczr  21792  cygzn  21882  lmiclbs  22149  lmisfree  22154  lmictra  22157  mpfrcl  22400  ply1frcl  22642  mdetdiaglem  22919  mdet0  22927  toponmre  23417  iunconnlem  23751  iunconn  23752  unconn  23753  clsconn  23754  2ndcdisj  23781  2ndcsep  23784  1stcelcls  23786  locfincmp  23851  comppfsc  23857  txcls  23929  hmphsym  24107  hmphtr  24108  hmphen  24110  haushmphlem  24112  cmphmph  24113  connhmph  24114  reghmph  24118  nrmhmph  24119  hmphdis  24121  hmphen2  24124  fbdmn0  24159  isfbas2  24160  fbssint  24163  trfbas2  24168  filtop  24180  isfil2  24181  elfg  24196  fgcl  24203  filssufilg  24236  uffix2  24249  ufildom1  24251  hauspwpwf1  24312  hausflf2  24323  alexsubALTlem2  24373  ptcmplem2  24378  cnextf  24391  tgptsmscld  24476  ustfilxp  24538  xbln0  24739  lpbl  24828  met2ndci  24847  metustfbas  24882  restmetu  24895  reconn  25154  opnreen  25157  metdsre  25179  phtpcer  25322  phtpc01  25323  phtpcco2  25326  pcohtpy  25347  cfilfcls  25601  cmetcaulem  25615  cmetcau  25616  bcthlem5  25655  ovolicc2lem2  25845  ovolicc2lem5  25848  ioorcl2  25899  ioorinv2  25902  itg11  26018  dvlip  26319  dvne0  26337  fta1g  26494  plyssc  26524  fta1  26635  vieta1lem2  26640  nobdaymin  28145  sltstr  28179  ltslpss  28300  lrrecfr  28335  oncutlt  28656  hpgerlem  29249  axcontlem4  29551  axcontlem10  29557  upgrex  29676  fusgrn0degnn0  30086  uhgrvd00  30121  wspthsnonn0vne  30512  eulerpath  30848  frgrwopreglem2  30920  ubthlem1  31478  shintcli  31937  2ndimaxp  33288  fpwrelmapffslem  33371  qsdrng  34068  1arithidom  34116  dimcl  34282  lmimdim  34283  lmicdim  34284  lvecdim0i  34285  lvecdim0  34286  lssdimle  34287  dimpropd  34288  dimkerim  34306  fedgmul  34310  extdg1id  34345  fmcncfil  34610  insiga  34817  unelldsys  34838  bnj1189  35686  bnj1279  35695  soinfdom  35769  rankscott  35807  axregszf  35854  karddom  35886  kardsdom  35887  vonf1oonfo  35969  pconnconn  36083  txsconn  36093  cvmsss2  36126  cvmopnlem  36130  cvmfolem  36131  cvmliftmolem2  36134  cvmlift2lem10  36164  cvmliftpht  36170  cvmlift3lem8  36178  eldm3  36619  fundmpss  36625  elima4  36633  neibastop1  37240  neibastop2lem  37241  neibastop2  37242  fnemeet2  37248  fnejoin2  37250  neifg  37252  tailfb  37258  filnetlem3  37261  mh-infprim1bi  37427  bj-n0i  37957  bj-rest10  38102  bj-restn0  38104  poimirlem30  38662  itg2addnclem2  38684  prdsbnd2  38823  heibor1lem  38837  bfp  38852  divrngidl  39056  eldmres3  39309  rnxrn  39447  eldmxrncnvepres2  39461  trcoss2  39600  atex  40557  llnn0  40667  lplnn0N  40698  lvoln0N  40742  pmapglb2N  40922  pmapglb2xN  40923  elpaddn0  40951  osumcllem8N  41114  pexmidlem5N  41125  diaglbN  42206  diaintclN  42209  dibglbN  42317  dibintclN  42318  dihglblem2aN  42444  dihglblem5  42449  dihglbcpreN  42451  dihintcl  42495  unitscyglem5  43343  riccrng1  43676  ricdrng1  43686  rencldnfilem  43921  kelac1  44159  lnmlmic  44184  gicabl  44195  neik0pk1imk0  45141  ntrneineine0lem  45177  onfrALT  45626  onfrALTVD  45967  iunconnlem2  46011  relpfrlem  46037  dfac5prim  46074  permac8prim  46098  snelmap  46193  eliin2f  46213  disjinfi  46301  mapss2  46313  difmap  46314  infrpge  46457  infxrlesupxr  46540  inficc  46640  fsumnncl  46678  ellimciota  46720  islpcn  46743  lptre2pt  46744  stoweidlem35  47139  fourierdlem31  47242  fourier2  47331  qndenserrnbllem  47398  qndenserrnopn  47402  qndenserrn  47403  intsaluni  47433  sge0cl  47485  ovn0lem  47669  ovnsubaddlem2  47675  hoidmvval0b  47694  hspdifhsp  47720  fsetprcnexALT  48226  uniimaelsetpreimafv  48572  imasetpreimafvbijlemfv1  48579  dfgric2  49107  gricuspgr  49110  gricsym  49113  grictr  49115  gricen  49117  dfgrlic2  49200  dfgrlic3  49202  grlicen  49209  gricgrlic  49210  usgrexmpl12ngric  49230  usgrexmpl12ngrlic  49231  opmpoismgm  49358  neircl  50113  sectrcl  50230  invrcl  50232  isorcl  50241  iinfssc  50265  iinfsubc  50266  imaid  50364  thincn0eu  50660  thinccic  50700  termcterm2  50743  eufunc  50751  euendfunc  50755  diag1f1o  50763  diag2f1o  50769  prstchom2ALT  50796  rellan  50900  relran  50901  alsralrex  51077