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 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 2961	. 2 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
2		neq0 4307	. 2 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
3	1, 2	bitri 278	1 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1563  ∃wex 1802   ∈ wcel 2145   ≠ wne 2960  ∅c0 4288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-ne 2961  df-dif 3910  df-nul 4289

This theorem is referenced by:  n0limd  4309  reximdva0  4311  rspn0  4312  n0rex  4313  n0moeu  4315  eqeuel  4321  ndisj  4326  pssnel  4428  r19.2z  4456  r19.3rz  4458  uniintsn  4945  iunn0  5026  trintss  5230  intex  5304  notzfaus  5324  reusv2lem1  5359  nnullss  5433  exss  5434  opabn0  5528  wefrc  5645  wereu2  5648  dmxp  5909  xpnz  6147  dmsnn0  6197  unixp0  6273  xpco  6279  frpomin  6330  onfr  6389  iotanul2  6498  fveqdmss  7063  eldmrexrnb  7077  isofrlem  7328  limuni3  7836  soex  7906  f1oweALT  7957  fo1stres  8000  fo2ndres  8001  ecdmn0  8735  fsetprcnex  8847  map0g  8870  ixpn0  8916  resixpfo  8922  domdifsn  9036  xpdom3  9051  fodomr  9104  mapdom3  9125  0sdom1dom  9194  unblem2  9241  fodomfir  9275  marypha1lem  9381  brwdom2  9523  unxpwdom2  9538  ixpiunwdom  9540  zfreg  9546  epfrs  9688  frmin  9709  scott0  9848  scotteld  9860  cplem1  9863  fseqen  9999  finacn  10022  iunfictbso  10086  aceq2  10091  dfac3  10093  dfac9  10108  kmlem6  10127  kmlem8  10129  infpss  10187  fin23lem7  10288  enfin2i  10293  fin23lem21  10311  fin23lem31  10315  isf32lem9  10333  isf34lem4  10349  axdc2lem  10420  axdc3lem4  10425  ac6c4  10453  ac9  10455  ac6s4  10462  ac9s  10465  ttukeyg  10489  fpwwe2lem11  10614  wun0  10691  tsk0  10736  gruina  10791  genpn0  10976  prlem934  11006  ltaddpr  11007  ltexprlem1  11009  prlem936  11020  reclem2pr  11021  suplem1pr  11025  supsr  11085  axpre-sup  11142  dedekind  11361  dedekindle  11362  negn0  11631  infm3  12162  supaddc  12170  supadd  12171  supmul1  12172  supmullem2  12174  supmul  12175  zsupss  12949  xrsupsslem  13321  xrinfmsslem  13322  supxrre  13341  infxrre  13351  ixxub  13381  ixxlb  13382  ioorebas  13466  fzn0  13554  fzon0  13694  hashgt0elexb  14426  swrdcl  14671  pfxcl  14703  maxprmfct  16756  4sqlem12  17004  vdwmc  17026  ramz  17073  ramub1  17076  mreiincl  17636  mremre  17644  mreexexlem4d  17691  iscatd2  17725  catcone0  17731  cic  17844  drsdirfi  18349  mgmpropd  18697  opifismgm  18705  dfgrp3lem  19092  dfgrp3e  19094  issubg2  19196  subgint  19205  qsxpid  19231  giclcl  19331  gicrcl  19332  gicsym  19333  gictr  19334  gicen  19336  gicsubgen  19337  cntzssv  19386  symggen  19528  psgnunilem3  19554  sylow1lem4  19659  odcau  19662  sylow3  19691  cyggex2  19955  giccyg  19958  pgpfac1lem5  20139  ricsym  20576  brric2  20577  subrngint  20633  subrgint  20668  abvn0b  20905  lss0cl  21034  lmiclcl  21157  lmicrcl  21158  lmicsym  21159  lspsnat  21235  lspprat  21243  lidlunin0  21327  qsidomlem2  21438  cnsubrg  21534  nzerooringczr  21587  cygzn  21677  lmiclbs  21944  lmisfree  21949  lmictra  21952  mpfrcl  22193  ply1frcl  22435  mdetdiaglem  22712  mdet0  22720  toponmre  23207  iunconnlem  23541  iunconn  23542  unconn  23543  clsconn  23544  2ndcdisj  23570  2ndcsep  23573  1stcelcls  23575  locfincmp  23640  comppfsc  23646  txcls  23718  hmphsym  23896  hmphtr  23897  hmphen  23899  haushmphlem  23901  cmphmph  23902  connhmph  23903  reghmph  23907  nrmhmph  23908  hmphdis  23910  hmphen2  23913  fbdmn0  23948  isfbas2  23949  fbssint  23952  trfbas2  23957  filtop  23969  isfil2  23970  elfg  23985  fgcl  23992  filssufilg  24025  uffix2  24038  ufildom1  24040  hauspwpwf1  24101  hausflf2  24112  alexsubALTlem2  24162  ptcmplem2  24167  cnextf  24180  tgptsmscld  24265  ustfilxp  24327  xbln0  24528  lpbl  24617  met2ndci  24636  metustfbas  24671  restmetu  24684  reconn  24943  opnreen  24946  metdsre  24968  phtpcer  25111  phtpc01  25112  phtpcco2  25115  pcohtpy  25136  cfilfcls  25390  cmetcaulem  25404  cmetcau  25405  bcthlem5  25444  ovolicc2lem2  25634  ovolicc2lem5  25637  ioorcl2  25688  ioorinv2  25691  itg11  25807  dvlip  26109  dvne0  26127  fta1g  26284  plyssc  26314  fta1  26426  vieta1lem2  26429  nobdaymin  27900  sltstr  27934  ltslpss  28055  lrrecfr  28090  oncutlt  28411  hpgerlem  28992  axcontlem4  29222  axcontlem10  29228  upgrex  29347  fusgrn0degnn0  29754  uhgrvd00  29789  wspthsnonn0vne  30171  eulerpath  30497  frgrwopreglem2  30569  ubthlem1  31127  shintcli  31586  2ndimaxp  32899  fpwrelmapffslem  32985  qsdrng  33691  1arithidom  33739  dimcl  33905  lmimdim  33906  lmicdim  33907  lvecdim0i  33908  lvecdim0  33909  lssdimle  33910  dimpropd  33911  dimkerim  33929  fedgmul  33933  extdg1id  33968  fmcncfil  34233  insiga  34439  unelldsys  34460  bnj1189  35309  bnj1279  35318  axregszf  35432  vonf1oonfo  35465  pconnconn  35589  txsconn  35599  cvmsss2  35632  cvmopnlem  35636  cvmfolem  35637  cvmliftmolem2  35640  cvmlift2lem10  35670  cvmliftpht  35676  cvmlift3lem8  35684  eldm3  36119  fundmpss  36125  elima4  36134  neibastop1  36727  neibastop2lem  36728  neibastop2  36729  fnemeet2  36735  fnejoin2  36737  neifg  36739  tailfb  36745  filnetlem3  36748  mh-infprim1bi  36914  bj-n0i  37443  bj-rest10  37585  bj-restn0  37587  poimirlem30  38156  itg2addnclem2  38178  prdsbnd2  38301  heibor1lem  38315  bfp  38330  divrngidl  38534  eldmres3  38789  rnxrn  38927  eldmxrncnvepres2  38941  trcoss2  39080  atex  40037  llnn0  40147  lplnn0N  40178  lvoln0N  40222  pmapglb2N  40402  pmapglb2xN  40403  elpaddn0  40431  osumcllem8N  40594  pexmidlem5N  40605  diaglbN  41686  diaintclN  41689  dibglbN  41797  dibintclN  41798  dihglblem2aN  41924  dihglblem5  41929  dihglbcpreN  41931  dihintcl  41975  unitscyglem5  42823  rictr  43145  riccrng1  43146  ricdrng1  43153  rencldnfilem  43404  kelac1  43647  lnmlmic  43672  gicabl  43683  neik0pk1imk0  44630  ntrneineine0lem  44666  onfrALT  45117  onfrALTVD  45458  iunconnlem2  45502  relpfrlem  45521  dfac5prim  45558  permac8prim  45582  snelmap  45661  eliin2f  45681  disjinfi  45769  mapss2  45781  difmap  45782  infrpge  45926  infxrlesupxr  46009  inficc  46109  fsumnncl  46147  ellimciota  46189  islpcn  46212  lptre2pt  46213  stoweidlem35  46608  fourierdlem31  46711  fourier2  46800  qndenserrnbllem  46867  qndenserrnopn  46871  qndenserrn  46872  intsaluni  46902  sge0cl  46954  ovn0lem  47138  ovnsubaddlem2  47144  hoidmvval0b  47163  hspdifhsp  47189  fsetprcnexALT  47655  uniimaelsetpreimafv  48001  imasetpreimafvbijlemfv1  48008  dfgric2  48536  gricuspgr  48539  gricsym  48542  grictr  48544  gricen  48546  dfgrlic2  48629  dfgrlic3  48631  grlicen  48638  gricgrlic  48639  usgrexmpl12ngric  48659  usgrexmpl12ngrlic  48660  opmpoismgm  48788  neircl  49535  sectrcl  49652  invrcl  49654  isorcl  49663  iinfssc  49687  iinfsubc  49688  imaid  49784  thincn0eu  50061  thinccic  50101  termcterm2  50144  eufunc  50152  euendfunc  50156  diag1f1o  50164  diag2f1o  50167  prstchom2ALT  50194  rellan  50253  relran  50254  alscn0d  50425