Theorem n0 4280

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 2154, ax-12 2171. (Revised by Gino Giotto, 28-Jun-2024.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1539  ∃wex 1782   ∈ wcel 2106   ≠ wne 2943  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-ne 2944  df-dif 3890  df-nul 4257

This theorem is referenced by:  reximdva0  4285  rspn0  4286  rspn0OLD  4287  n0rex  4288  n0moeu  4290  eqeuel  4296  ndisj  4301  pssnel  4404  r19.2z  4425  r19.2zb  4426  r19.3rz  4427  uniintsn  4918  iunn0  4996  trintss  5208  intex  5261  notzfaus  5285  reusv2lem1  5321  nnullss  5377  exss  5378  opabn0  5466  wefrc  5583  wereu2  5586  dmxp  5838  xpnz  6062  dmsnn0  6110  unixp0  6186  xpco  6192  frpomin  6243  onfr  6305  fveqdmss  6956  eldmrexrnb  6968  isofrlem  7211  limuni3  7699  soex  7768  f1oweALT  7815  fo1stres  7857  fo2ndres  7858  ecdmn0  8545  fsetprcnex  8650  map0g  8672  ixpn0  8718  resixpfo  8724  domdifsn  8841  xpdom3  8857  fodomr  8915  mapdom3  8936  findcard2OLD  9056  unblem2  9067  marypha1lem  9192  brwdom2  9332  unxpwdom2  9347  ixpiunwdom  9349  zfreg  9354  epfrs  9489  frmin  9507  scott0  9644  cplem1  9647  fseqen  9783  finacn  9806  iunfictbso  9870  aceq2  9875  dfac3  9877  dfac9  9892  kmlem6  9911  kmlem8  9913  infpss  9973  fin23lem7  10072  enfin2i  10077  fin23lem21  10095  fin23lem31  10099  isf32lem9  10117  isf34lem4  10133  axdc2lem  10204  axdc3lem4  10209  ac6c4  10237  ac9  10239  ac6s4  10246  ac9s  10249  ttukeyg  10273  fpwwe2lem11  10397  wun0  10474  tsk0  10519  gruina  10574  genpn0  10759  prlem934  10789  ltaddpr  10790  ltexprlem1  10792  prlem936  10803  reclem2pr  10804  suplem1pr  10808  supsr  10868  axpre-sup  10925  dedekind  11138  dedekindle  11139  negn0  11404  infm3  11934  supaddc  11942  supadd  11943  supmul1  11944  supmullem2  11946  supmul  11947  zsupss  12677  xrsupsslem  13041  xrinfmsslem  13042  supxrre  13061  infxrre  13070  ixxub  13100  ixxlb  13101  ioorebas  13183  fzn0  13270  fzon0  13405  hashgt0elexb  14117  swrdcl  14358  pfxcl  14390  maxprmfct  16414  4sqlem12  16657  vdwmc  16679  ramz  16726  ramub1  16729  mreiincl  17305  mremre  17313  mreexexlem4d  17356  iscatd2  17390  catcone0  17396  cic  17511  drsdirfi  18023  opifismgm  18343  dfgrp3lem  18673  dfgrp3e  18675  issubg2  18770  subgint  18779  giclcl  18888  gicrcl  18889  gicsym  18890  gictr  18891  gicen  18893  gicsubgen  18894  cntzssv  18934  symggen  19078  psgnunilem3  19104  sylow1lem4  19206  odcau  19209  sylow3  19238  cyggex2  19498  giccyg  19501  pgpfac1lem5  19682  brric2  19989  subrgint  20046  lss0cl  20208  lmiclcl  20332  lmicrcl  20333  lmicsym  20334  lspsnat  20407  lspprat  20415  abvn0b  20573  cnsubrg  20658  cygzn  20778  lmiclbs  21044  lmisfree  21049  lmictra  21052  mpfrcl  21295  ply1frcl  21484  mdetdiaglem  21747  mdet0  21755  toponmre  22244  iunconnlem  22578  iunconn  22579  unconn  22580  clsconn  22581  2ndcdisj  22607  2ndcsep  22610  1stcelcls  22612  locfincmp  22677  comppfsc  22683  txcls  22755  hmphsym  22933  hmphtr  22934  hmphen  22936  haushmphlem  22938  cmphmph  22939  connhmph  22940  reghmph  22944  nrmhmph  22945  hmphdis  22947  hmphen2  22950  fbdmn0  22985  isfbas2  22986  fbssint  22989  trfbas2  22994  filtop  23006  isfil2  23007  elfg  23022  fgcl  23029  filssufilg  23062  uffix2  23075  ufildom1  23077  hauspwpwf1  23138  hausflf2  23149  alexsubALTlem2  23199  ptcmplem2  23204  cnextf  23217  tgptsmscld  23302  ustfilxp  23364  xbln0  23567  lpbl  23659  met2ndci  23678  metustfbas  23713  restmetu  23726  reconn  23991  opnreen  23994  metdsre  24016  phtpcer  24158  phtpc01  24159  phtpcco2  24162  pcohtpy  24183  cfilfcls  24438  cmetcaulem  24452  cmetcau  24453  bcthlem5  24492  ovolicc2lem2  24682  ovolicc2lem5  24685  ioorcl2  24736  ioorinv2  24739  itg11  24855  dvlip  25157  dvne0  25175  fta1g  25332  plyssc  25361  fta1  25468  vieta1lem2  25471  hpgerlem  27126  axcontlem4  27335  axcontlem10  27341  upgrex  27462  fusgrn0degnn0  27866  uhgrvd00  27901  wspthsnonn0vne  28282  eulerpath  28605  frgrwopreglem2  28677  ubthlem1  29232  shintcli  29691  2ndimaxp  30984  fpwrelmapffslem  31067  qsxpid  31558  qsidomlem2  31629  dimcl  31688  lvecdim0i  31689  lvecdim0  31690  lssdimle  31691  dimpropd  31692  dimkerim  31708  fedgmul  31712  extdg1id  31738  fmcncfil  31881  insiga  32105  unelldsys  32126  bnj521  32716  bnj1189  32989  bnj1279  32998  pconnconn  33193  txsconn  33203  cvmsss2  33236  cvmopnlem  33240  cvmfolem  33241  cvmliftmolem2  33244  cvmlift2lem10  33274  cvmliftpht  33280  cvmlift3lem8  33288  eldm3  33728  fundmpss  33740  elima4  33750  nocvxmin  33973  sslttr  34001  sltlpss  34087  lrrecfr  34100  neibastop1  34548  neibastop2lem  34549  neibastop2  34550  fnemeet2  34556  fnejoin2  34558  neifg  34560  tailfb  34566  filnetlem3  34569  bj-n0i  35140  bj-rest10  35259  bj-restn0  35261  poimirlem30  35807  itg2addnclem2  35829  prdsbnd2  35953  heibor1lem  35967  bfp  35982  divrngidl  36186  rnxrn  36524  trcoss2  36602  atex  37420  llnn0  37530  lplnn0N  37561  lvoln0N  37605  pmapglb2N  37785  pmapglb2xN  37786  elpaddn0  37814  osumcllem8N  37977  pexmidlem5N  37988  diaglbN  39069  diaintclN  39072  dibglbN  39180  dibintclN  39181  dihglblem2aN  39307  dihglblem5  39312  dihglbcpreN  39314  dihintcl  39358  sn-iotanul  40194  rencldnfilem  40642  kelac1  40888  lnmlmic  40913  gicabl  40924  neik0pk1imk0  41657  ntrneineine0lem  41693  scotteld  41864  onfrALT  42169  onfrALTVD  42511  iunconnlem2  42555  snelmap  42632  eliin2f  42654  disjinfi  42731  mapss2  42745  difmap  42747  infrpge  42890  infxrlesupxr  42976  inficc  43072  fsumnncl  43113  ellimciota  43155  islpcn  43180  lptre2pt  43181  stoweidlem35  43576  fourierdlem31  43679  fourier2  43768  qndenserrnbllem  43835  qndenserrnopn  43839  qndenserrn  43840  intsaluni  43868  sge0cl  43919  ovn0lem  44103  ovnsubaddlem2  44109  hoidmvval0b  44128  hspdifhsp  44154  fsetprcnexALT  44556  uniimaelsetpreimafv  44848  imasetpreimafvbijlemfv1  44855  mgmpropd  45329  opmpoismgm  45361  nzerooringczr  45630  neircl  46198  thincn0eu  46313  thinccic  46342  prstchom2ALT  46360  alscn0d  46499