Theorem n0 4303

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2957  ∅c0 4282

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-ne 2958  df-dif 3905  df-nul 4283

This theorem is used by:  n0limd  4304  reximdva0  4306  rspn0  4307  n0rex  4308  n0moeu  4310  eqeuel  4316  ndisj  4321  pssnel  4427  r19.2z  4458  r19.3rz  4460  uniintsn  4948  iunn0  5029  trintss  5235  intex  5312  notsep  5332  reusv2lem1  5367  nnullss  5441  exss  5442  opabn0  5536  wefrc  5653  wereu2  5656  dmxp  5917  xpnz  6155  dmsnn0  6207  unixp0  6285  xpco  6291  frpomin  6342  onfr  6401  iotanul2  6510  fveqdmss  7074  eldmrexrnb  7088  isofrlem  7344  limuni3  7851  soex  7921  f1oweALT  7972  fo1stres  8015  fo2ndres  8016  ecdmn0  8752  fsetprcnex  8866  map0g  8894  ixpn0  8940  resixpfo  8946  domdifsn  9061  xpdom3  9076  fodomr  9129  mapdom3  9150  0sdom1dom  9219  unblem2  9266  fodomfir  9300  marypha1lem  9406  brwdom2  9548  unxpwdom2  9563  ixpiunwdom  9565  zfreg  9571  epfrs  9713  frmin  9734  scott0b  9879  scott0OLD  9880  scotteld  9889  cplem1  9892  cplem1OLD  9893  karden  9901  fseqen  10033  finacn  10056  iunfictbso  10120  aceq2  10125  dfac3  10127  dfac9  10142  kmlem6  10161  kmlem8  10163  infpss  10221  fin23lem7  10321  enfin2i  10326  fin23lem21  10344  fin23lem31  10348  isf32lem9  10366  isf34lem4  10382  axdc2lem  10453  axdc3lem4  10458  ac6c4  10486  ac9  10488  ac6s4  10495  ac9s  10498  ttukeyg  10522  fpwwe2lem11  10653  wun0  10730  tsk0  10775  gruina  10830  genpn0  11015  prlem934  11045  ltaddpr  11046  ltexprlem1  11048  prlem936  11059  reclem2pr  11060  suplem1pr  11064  supsr  11124  axpre-sup  11181  dedekind  11400  dedekindle  11401  negn0  11670  infm3  12201  supaddc  12209  supadd  12210  supmul1  12211  supmullem2  12213  supmul  12214  zsupss  12989  xrsupsslem  13361  xrinfmsslem  13362  supxrre  13381  infxrre  13391  ixxub  13421  ixxlb  13422  ioorebas  13506  fzn0  13594  fzon0  13735  hashgt0elexb  14468  swrdcl  14715  pfxcl  14749  maxprmfct  16804  4sqlem12  17052  vdwmc  17074  ramz  17121  ramub1  17124  mreiincl  17684  mremre  17692  mreexexlem4d  17739  iscatd2  17773  catcone0  17779  cic  17892  drsdirfi  18397  mgmpropd  18747  opifismgm  18755  dfgrp3lem  19162  dfgrp3e  19164  issubg2  19266  subgint  19275  qsxpid  19301  giclcl  19401  gicrcl  19402  gicsym  19403  gictr  19404  gicen  19406  gicsubgen  19407  cntzssv  19456  symggen  19598  psgnunilem3  19624  sylow1lem4  19729  odcau  19732  sylow3  19761  cyggex2  20025  giccyg  20028  pgpfac1lem5  20209  riclcl  20661  ricrcl  20662  ricsym  20663  rictr  20664  isbrric2  20665  subrngint  20723  subrgint  20758  abvn0b  21003  lss0cl  21132  lmiclcl  21255  lmicrcl  21256  lmicsym  21257  lspsnat  21333  lspprat  21341  lidlunin0  21425  qsidomlem2  21545  cnsubrg  21641  nzerooringczr  21694  cygzn  21784  lmiclbs  22051  lmisfree  22056  lmictra  22059  mpfrcl  22302  ply1frcl  22544  mdetdiaglem  22821  mdet0  22829  toponmre  23319  iunconnlem  23653  iunconn  23654  unconn  23655  clsconn  23656  2ndcdisj  23683  2ndcsep  23686  1stcelcls  23688  locfincmp  23753  comppfsc  23759  txcls  23831  hmphsym  24009  hmphtr  24010  hmphen  24012  haushmphlem  24014  cmphmph  24015  connhmph  24016  reghmph  24020  nrmhmph  24021  hmphdis  24023  hmphen2  24026  fbdmn0  24061  isfbas2  24062  fbssint  24065  trfbas2  24070  filtop  24082  isfil2  24083  elfg  24098  fgcl  24105  filssufilg  24138  uffix2  24151  ufildom1  24153  hauspwpwf1  24214  hausflf2  24225  alexsubALTlem2  24275  ptcmplem2  24280  cnextf  24293  tgptsmscld  24378  ustfilxp  24440  xbln0  24641  lpbl  24730  met2ndci  24749  metustfbas  24784  restmetu  24797  reconn  25056  opnreen  25059  metdsre  25081  phtpcer  25224  phtpc01  25225  phtpcco2  25228  pcohtpy  25249  cfilfcls  25503  cmetcaulem  25517  cmetcau  25518  bcthlem5  25557  ovolicc2lem2  25747  ovolicc2lem5  25750  ioorcl2  25801  ioorinv2  25804  itg11  25920  dvlip  26222  dvne0  26240  fta1g  26397  plyssc  26427  fta1  26539  vieta1lem2  26542  nobdaymin  28016  sltstr  28050  ltslpss  28171  lrrecfr  28206  oncutlt  28527  hpgerlem  29120  axcontlem4  29410  axcontlem10  29416  upgrex  29535  fusgrn0degnn0  29945  uhgrvd00  29980  wspthsnonn0vne  30371  eulerpath  30707  frgrwopreglem2  30779  ubthlem1  31337  shintcli  31796  2ndimaxp  33106  fpwrelmapffslem  33190  qsdrng  33886  1arithidom  33934  dimcl  34100  lmimdim  34101  lmicdim  34102  lvecdim0i  34103  lvecdim0  34104  lssdimle  34105  dimpropd  34106  dimkerim  34124  fedgmul  34128  extdg1id  34163  fmcncfil  34428  insiga  34635  unelldsys  34656  bnj1189  35505  bnj1279  35514  rankscott  35622  axregszf  35642  karddom  35674  kardsdom  35675  vonf1oonfo  35699  pconnconn  35797  txsconn  35807  cvmsss2  35840  cvmopnlem  35844  cvmfolem  35845  cvmliftmolem2  35848  cvmlift2lem10  35878  cvmliftpht  35884  cvmlift3lem8  35892  eldm3  36327  fundmpss  36333  elima4  36342  neibastop1  36965  neibastop2lem  36966  neibastop2  36967  fnemeet2  36973  fnejoin2  36975  neifg  36977  tailfb  36983  filnetlem3  36986  mh-infprim1bi  37152  bj-n0i  37682  bj-rest10  37825  bj-restn0  37827  poimirlem30  38386  itg2addnclem2  38408  prdsbnd2  38532  heibor1lem  38546  bfp  38561  divrngidl  38765  eldmres3  39018  rnxrn  39156  eldmxrncnvepres2  39170  trcoss2  39309  atex  40266  llnn0  40376  lplnn0N  40407  lvoln0N  40451  pmapglb2N  40631  pmapglb2xN  40632  elpaddn0  40660  osumcllem8N  40823  pexmidlem5N  40834  diaglbN  41915  diaintclN  41918  dibglbN  42026  dibintclN  42027  dihglblem2aN  42153  dihglblem5  42158  dihglbcpreN  42160  dihintcl  42204  unitscyglem5  43052  riccrng1  43390  ricdrng1  43397  rencldnfilem  43648  kelac1  43891  lnmlmic  43916  gicabl  43927  neik0pk1imk0  44874  ntrneineine0lem  44910  onfrALT  45359  onfrALTVD  45700  iunconnlem2  45744  relpfrlem  45763  dfac5prim  45800  permac8prim  45824  snelmap  45903  eliin2f  45923  disjinfi  46011  mapss2  46023  difmap  46024  infrpge  46168  infxrlesupxr  46251  inficc  46351  fsumnncl  46389  ellimciota  46431  islpcn  46454  lptre2pt  46455  stoweidlem35  46850  fourierdlem31  46953  fourier2  47042  qndenserrnbllem  47109  qndenserrnopn  47113  qndenserrn  47114  intsaluni  47144  sge0cl  47196  ovn0lem  47380  ovnsubaddlem2  47386  hoidmvval0b  47405  hspdifhsp  47431  fsetprcnexALT  47937  uniimaelsetpreimafv  48283  imasetpreimafvbijlemfv1  48290  dfgric2  48818  gricuspgr  48821  gricsym  48824  grictr  48826  gricen  48828  dfgrlic2  48911  dfgrlic3  48913  grlicen  48920  gricgrlic  48921  usgrexmpl12ngric  48941  usgrexmpl12ngrlic  48942  opmpoismgm  49069  neircl  49818  sectrcl  49935  invrcl  49937  isorcl  49946  iinfssc  49970  iinfsubc  49971  imaid  50067  thincn0eu  50344  thinccic  50384  termcterm2  50427  eufunc  50435  euendfunc  50439  diag1f1o  50447  diag2f1o  50450  prstchom2ALT  50477  rellan  50536  relran  50537  alsralrex  50728