Theorem n0 4294

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2933  ∅c0 4274

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ne 2934  df-dif 3893  df-nul 4275

This theorem is referenced by:  reximdva0  4296  rspn0  4297  n0rex  4298  n0moeu  4300  eqeuel  4306  ndisj  4311  pssnel  4412  r19.2z  4440  r19.3rz  4442  uniintsn  4928  iunn0  5010  trintss  5211  intex  5281  notzfaus  5300  reusv2lem1  5335  nnullss  5409  exss  5410  opabn0  5501  wefrc  5618  wereu2  5621  dmxp  5878  xpnz  6117  dmsnn0  6165  unixp0  6241  xpco  6247  frpomin  6298  onfr  6356  iotanul2  6465  fveqdmss  7024  eldmrexrnb  7038  isofrlem  7288  limuni3  7796  soex  7865  f1oweALT  7918  fo1stres  7961  fo2ndres  7962  ecdmn0  8689  fsetprcnex  8802  map0g  8825  ixpn0  8871  resixpfo  8877  domdifsn  8991  xpdom3  9006  fodomr  9059  mapdom3  9080  0sdom1dom  9149  unblem2  9196  fodomfir  9231  marypha1lem  9339  brwdom2  9481  unxpwdom2  9496  ixpiunwdom  9498  zfreg  9504  epfrs  9643  frmin  9664  scott0  9801  cplem1  9804  fseqen  9940  finacn  9963  iunfictbso  10027  aceq2  10032  dfac3  10034  dfac9  10050  kmlem6  10069  kmlem8  10071  infpss  10129  fin23lem7  10229  enfin2i  10234  fin23lem21  10252  fin23lem31  10256  isf32lem9  10274  isf34lem4  10290  axdc2lem  10361  axdc3lem4  10366  ac6c4  10394  ac9  10396  ac6s4  10403  ac9s  10406  ttukeyg  10430  fpwwe2lem11  10555  wun0  10632  tsk0  10677  gruina  10732  genpn0  10917  prlem934  10947  ltaddpr  10948  ltexprlem1  10950  prlem936  10961  reclem2pr  10962  suplem1pr  10966  supsr  11026  axpre-sup  11083  dedekind  11300  dedekindle  11301  negn0  11570  infm3  12106  supaddc  12114  supadd  12115  supmul1  12116  supmullem2  12118  supmul  12119  zsupss  12878  xrsupsslem  13250  xrinfmsslem  13251  supxrre  13270  infxrre  13280  ixxub  13310  ixxlb  13311  ioorebas  13395  fzn0  13483  fzon0  13623  hashgt0elexb  14355  swrdcl  14599  pfxcl  14631  maxprmfct  16670  4sqlem12  16918  vdwmc  16940  ramz  16987  ramub1  16990  mreiincl  17549  mremre  17557  mreexexlem4d  17604  iscatd2  17638  catcone0  17644  cic  17757  drsdirfi  18262  mgmpropd  18610  opifismgm  18618  dfgrp3lem  19005  dfgrp3e  19007  issubg2  19108  subgint  19117  giclcl  19239  gicrcl  19240  gicsym  19241  gictr  19242  gicen  19244  gicsubgen  19245  cntzssv  19294  symggen  19436  psgnunilem3  19462  sylow1lem4  19567  odcau  19570  sylow3  19599  cyggex2  19863  giccyg  19866  pgpfac1lem5  20047  brric2  20474  subrngint  20528  subrgint  20563  abvn0b  20804  lss0cl  20933  lmiclcl  21057  lmicrcl  21058  lmicsym  21059  lspsnat  21135  lspprat  21143  cnsubrg  21417  nzerooringczr  21470  cygzn  21560  lmiclbs  21827  lmisfree  21832  lmictra  21835  mpfrcl  22073  ply1frcl  22293  mdetdiaglem  22573  mdet0  22581  toponmre  23068  iunconnlem  23402  iunconn  23403  unconn  23404  clsconn  23405  2ndcdisj  23431  2ndcsep  23434  1stcelcls  23436  locfincmp  23501  comppfsc  23507  txcls  23579  hmphsym  23757  hmphtr  23758  hmphen  23760  haushmphlem  23762  cmphmph  23763  connhmph  23764  reghmph  23768  nrmhmph  23769  hmphdis  23771  hmphen2  23774  fbdmn0  23809  isfbas2  23810  fbssint  23813  trfbas2  23818  filtop  23830  isfil2  23831  elfg  23846  fgcl  23853  filssufilg  23886  uffix2  23899  ufildom1  23901  hauspwpwf1  23962  hausflf2  23973  alexsubALTlem2  24023  ptcmplem2  24028  cnextf  24041  tgptsmscld  24126  ustfilxp  24188  xbln0  24389  lpbl  24478  met2ndci  24497  metustfbas  24532  restmetu  24545  reconn  24804  opnreen  24807  metdsre  24829  phtpcer  24972  phtpc01  24973  phtpcco2  24976  pcohtpy  24997  cfilfcls  25251  cmetcaulem  25265  cmetcau  25266  bcthlem5  25305  ovolicc2lem2  25495  ovolicc2lem5  25498  ioorcl2  25549  ioorinv2  25552  itg11  25668  dvlip  25970  dvne0  25988  fta1g  26145  plyssc  26175  fta1  26285  vieta1lem2  26288  nobdaymin  27759  sltstr  27793  ltslpss  27914  lrrecfr  27949  oncutlt  28270  hpgerlem  28847  axcontlem4  29050  axcontlem10  29056  upgrex  29175  fusgrn0degnn0  29583  uhgrvd00  29618  wspthsnonn0vne  30000  eulerpath  30326  frgrwopreglem2  30398  ubthlem1  30956  shintcli  31415  n0limd  32556  2ndimaxp  32734  fpwrelmapffslem  32820  qsxpid  33437  qsidomlem2  33528  qsdrng  33572  1arithidom  33612  dimcl  33762  lmimdim  33763  lmicdim  33764  lvecdim0i  33765  lvecdim0  33766  lssdimle  33767  dimpropd  33768  dimkerim  33787  fedgmul  33791  extdg1id  33826  fmcncfil  34091  insiga  34297  unelldsys  34318  bnj1189  35167  bnj1279  35176  axregszf  35289  pconnconn  35429  txsconn  35439  cvmsss2  35472  cvmopnlem  35476  cvmfolem  35477  cvmliftmolem2  35480  cvmlift2lem10  35510  cvmliftpht  35516  cvmlift3lem8  35524  eldm3  35959  fundmpss  35965  elima4  35974  neibastop1  36557  neibastop2lem  36558  neibastop2  36559  fnemeet2  36565  fnejoin2  36567  neifg  36569  tailfb  36575  filnetlem3  36578  mh-infprim1bi  36744  bj-n0i  37274  bj-rest10  37416  bj-restn0  37418  poimirlem30  37985  itg2addnclem2  38007  prdsbnd2  38130  heibor1lem  38144  bfp  38159  divrngidl  38363  eldmres3  38618  rnxrn  38756  eldmxrncnvepres2  38770  trcoss2  38909  atex  39866  llnn0  39976  lplnn0N  40007  lvoln0N  40051  pmapglb2N  40231  pmapglb2xN  40232  elpaddn0  40260  osumcllem8N  40423  pexmidlem5N  40434  diaglbN  41515  diaintclN  41518  dibglbN  41626  dibintclN  41627  dihglblem2aN  41753  dihglblem5  41758  dihglbcpreN  41760  dihintcl  41804  unitscyglem5  42652  ricsym  42978  rictr  42979  riccrng1  42980  ricdrng1  42987  rencldnfilem  43266  kelac1  43509  lnmlmic  43534  gicabl  43545  neik0pk1imk0  44492  ntrneineine0lem  44528  scotteld  44691  onfrALT  44994  onfrALTVD  45335  iunconnlem2  45379  relpfrlem  45398  dfac5prim  45435  permac8prim  45459  snelmap  45531  eliin2f  45552  disjinfi  45640  mapss2  45652  difmap  45654  infrpge  45799  infxrlesupxr  45882  inficc  45982  fsumnncl  46020  ellimciota  46062  islpcn  46085  lptre2pt  46086  stoweidlem35  46481  fourierdlem31  46584  fourier2  46673  qndenserrnbllem  46740  qndenserrnopn  46744  qndenserrn  46745  intsaluni  46775  sge0cl  46827  ovn0lem  47011  ovnsubaddlem2  47017  hoidmvval0b  47036  hspdifhsp  47062  fsetprcnexALT  47522  uniimaelsetpreimafv  47868  imasetpreimafvbijlemfv1  47875  dfgric2  48403  gricuspgr  48406  gricsym  48409  grictr  48411  gricen  48413  dfgrlic2  48496  dfgrlic3  48498  grlicen  48505  gricgrlic  48506  usgrexmpl12ngric  48526  usgrexmpl12ngrlic  48527  opmpoismgm  48655  neircl  49392  sectrcl  49509  invrcl  49511  isorcl  49520  iinfssc  49544  iinfsubc  49545  imaid  49641  thincn0eu  49918  thinccic  49958  termcterm2  50001  eufunc  50009  euendfunc  50013  diag1f1o  50021  diag2f1o  50024  prstchom2ALT  50051  rellan  50110  relran  50111  alscn0d  50282