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  7075  eldmrexrnb  7089  isofrlem  7345  limuni3  7852  soex  7922  f1oweALT  7973  fo1stres  8016  fo2ndres  8017  ecdmn0  8753  fsetprcnex  8867  map0g  8895  ixpn0  8941  resixpfo  8947  domdifsn  9062  xpdom3  9077  fodomr  9130  mapdom3  9151  0sdom1dom  9220  unblem2  9267  fodomfir  9301  marypha1lem  9407  brwdom2  9549  unxpwdom2  9564  ixpiunwdom  9566  zfreg  9572  epfrs  9714  frmin  9735  scott0b  9880  scott0OLD  9881  scotteld  9890  cplem1  9893  cplem1OLD  9894  karden  9902  fseqen  10034  finacn  10057  iunfictbso  10121  aceq2  10126  dfac3  10128  dfac9  10143  kmlem6  10162  kmlem8  10164  infpss  10222  fin23lem7  10322  enfin2i  10327  fin23lem21  10345  fin23lem31  10349  isf32lem9  10367  isf34lem4  10383  axdc2lem  10454  axdc3lem4  10459  ac6c4  10487  ac9  10489  ac6s4  10496  ac9s  10499  ttukeyg  10523  fpwwe2lem11  10654  wun0  10731  tsk0  10776  gruina  10831  genpn0  11016  prlem934  11046  ltaddpr  11047  ltexprlem1  11049  prlem936  11060  reclem2pr  11061  suplem1pr  11065  supsr  11125  axpre-sup  11182  dedekind  11401  dedekindle  11402  negn0  11671  infm3  12202  supaddc  12210  supadd  12211  supmul1  12212  supmullem2  12214  supmul  12215  zsupss  12990  xrsupsslem  13363  xrinfmsslem  13364  supxrre  13383  infxrre  13393  ixxub  13423  ixxlb  13424  ioorebas  13508  fzn0  13596  fzon0  13737  hashgt0elexb  14470  swrdcl  14717  pfxcl  14751  maxprmfct  16806  4sqlem12  17054  vdwmc  17076  ramz  17123  ramub1  17126  mreiincl  17686  mremre  17694  mreexexlem4d  17741  iscatd2  17775  catcone0  17781  cic  17894  drsdirfi  18399  mgmpropd  18749  opifismgm  18757  dfgrp3lem  19167  dfgrp3e  19169  issubg2  19271  subgint  19280  qsxpid  19306  giclcl  19406  gicrcl  19407  gicsym  19408  gictr  19409  gicen  19411  gicsubgen  19412  cntzssv  19461  symggen  19603  psgnunilem3  19629  sylow1lem4  19734  odcau  19737  sylow3  19766  cyggex2  20030  giccyg  20033  pgpfac1lem5  20214  riclcl  20666  ricrcl  20667  ricsym  20668  rictr  20669  isbrric2  20670  subrngint  20728  subrgint  20763  abvn0b  21008  lss0cl  21137  lmiclcl  21260  lmicrcl  21261  lmicsym  21262  lspsnat  21338  lspprat  21346  lidlunin0  21430  qsidomlem2  21550  cnsubrg  21646  nzerooringczr  21699  cygzn  21789  lmiclbs  22056  lmisfree  22061  lmictra  22064  mpfrcl  22307  ply1frcl  22549  mdetdiaglem  22826  mdet0  22834  toponmre  23324  iunconnlem  23658  iunconn  23659  unconn  23660  clsconn  23661  2ndcdisj  23688  2ndcsep  23691  1stcelcls  23693  locfincmp  23758  comppfsc  23764  txcls  23836  hmphsym  24014  hmphtr  24015  hmphen  24017  haushmphlem  24019  cmphmph  24020  connhmph  24021  reghmph  24025  nrmhmph  24026  hmphdis  24028  hmphen2  24031  fbdmn0  24066  isfbas2  24067  fbssint  24070  trfbas2  24075  filtop  24087  isfil2  24088  elfg  24103  fgcl  24110  filssufilg  24143  uffix2  24156  ufildom1  24158  hauspwpwf1  24219  hausflf2  24230  alexsubALTlem2  24280  ptcmplem2  24285  cnextf  24298  tgptsmscld  24383  ustfilxp  24445  xbln0  24646  lpbl  24735  met2ndci  24754  metustfbas  24789  restmetu  24802  reconn  25061  opnreen  25064  metdsre  25086  phtpcer  25229  phtpc01  25230  phtpcco2  25233  pcohtpy  25254  cfilfcls  25508  cmetcaulem  25522  cmetcau  25523  bcthlem5  25562  ovolicc2lem2  25752  ovolicc2lem5  25755  ioorcl2  25806  ioorinv2  25809  itg11  25925  dvlip  26227  dvne0  26245  fta1g  26402  plyssc  26432  fta1  26545  vieta1lem2  26550  nobdaymin  28026  sltstr  28060  ltslpss  28181  lrrecfr  28216  oncutlt  28537  hpgerlem  29130  axcontlem4  29432  axcontlem10  29438  upgrex  29557  fusgrn0degnn0  29967  uhgrvd00  30002  wspthsnonn0vne  30393  eulerpath  30729  frgrwopreglem2  30801  ubthlem1  31359  shintcli  31818  2ndimaxp  33127  fpwrelmapffslem  33211  qsdrng  33907  1arithidom  33955  dimcl  34121  lmimdim  34122  lmicdim  34123  lvecdim0i  34124  lvecdim0  34125  lssdimle  34126  dimpropd  34127  dimkerim  34145  fedgmul  34149  extdg1id  34184  fmcncfil  34449  insiga  34656  unelldsys  34677  bnj1189  35526  bnj1279  35535  rankscott  35643  axregszf  35663  karddom  35695  kardsdom  35696  vonf1oonfo  35720  pconnconn  35818  txsconn  35828  cvmsss2  35861  cvmopnlem  35865  cvmfolem  35866  cvmliftmolem2  35869  cvmlift2lem10  35899  cvmliftpht  35905  cvmlift3lem8  35913  eldm3  36348  fundmpss  36354  elima4  36363  neibastop1  36986  neibastop2lem  36987  neibastop2  36988  fnemeet2  36994  fnejoin2  36996  neifg  36998  tailfb  37004  filnetlem3  37007  mh-infprim1bi  37173  bj-n0i  37703  bj-rest10  37846  bj-restn0  37848  poimirlem30  38407  itg2addnclem2  38429  prdsbnd2  38553  heibor1lem  38567  bfp  38582  divrngidl  38786  eldmres3  39039  rnxrn  39177  eldmxrncnvepres2  39191  trcoss2  39330  atex  40287  llnn0  40397  lplnn0N  40428  lvoln0N  40472  pmapglb2N  40652  pmapglb2xN  40653  elpaddn0  40681  osumcllem8N  40844  pexmidlem5N  40855  diaglbN  41936  diaintclN  41939  dibglbN  42047  dibintclN  42048  dihglblem2aN  42174  dihglblem5  42179  dihglbcpreN  42181  dihintcl  42225  unitscyglem5  43073  riccrng1  43411  ricdrng1  43418  rencldnfilem  43669  kelac1  43912  lnmlmic  43937  gicabl  43948  neik0pk1imk0  44895  ntrneineine0lem  44931  onfrALT  45380  onfrALTVD  45721  iunconnlem2  45765  relpfrlem  45784  dfac5prim  45821  permac8prim  45845  snelmap  45924  eliin2f  45944  disjinfi  46032  mapss2  46044  difmap  46045  infrpge  46189  infxrlesupxr  46272  inficc  46372  fsumnncl  46410  ellimciota  46452  islpcn  46475  lptre2pt  46476  stoweidlem35  46871  fourierdlem31  46974  fourier2  47063  qndenserrnbllem  47130  qndenserrnopn  47134  qndenserrn  47135  intsaluni  47165  sge0cl  47217  ovn0lem  47401  ovnsubaddlem2  47407  hoidmvval0b  47426  hspdifhsp  47452  fsetprcnexALT  47958  uniimaelsetpreimafv  48304  imasetpreimafvbijlemfv1  48311  dfgric2  48839  gricuspgr  48842  gricsym  48845  grictr  48847  gricen  48849  dfgrlic2  48932  dfgrlic3  48934  grlicen  48941  gricgrlic  48942  usgrexmpl12ngric  48962  usgrexmpl12ngrlic  48963  opmpoismgm  49090  neircl  49839  sectrcl  49956  invrcl  49958  isorcl  49967  iinfssc  49991  iinfsubc  49992  imaid  50088  thincn0eu  50365  thinccic  50405  termcterm2  50448  eufunc  50456  euendfunc  50460  diag1f1o  50468  diag2f1o  50471  prstchom2ALT  50498  rellan  50557  relran  50558  alsralrex  50749