Theorem n0 4333

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1539  ∃wex 1778   ∈ wcel 2107   ≠ wne 2931  ∅c0 4313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-ne 2932  df-dif 3934  df-nul 4314

This theorem is referenced by:  reximdva0  4335  rspn0  4336  n0rex  4337  n0moeu  4339  eqeuel  4345  ndisj  4350  pssnel  4451  r19.2z  4475  r19.2zb  4476  r19.3rz  4477  uniintsn  4965  iunn0  5047  trintss  5258  intex  5324  notzfaus  5343  reusv2lem1  5378  nnullss  5447  exss  5448  opabn0  5538  wefrc  5659  wereu2  5662  dmxp  5919  dmxpOLD  5920  xpnz  6159  dmsnn0  6207  unixp0  6283  xpco  6289  frpomin  6340  onfr  6402  iotanul2  6511  fveqdmss  7078  eldmrexrnb  7092  isofrlem  7342  limuni3  7855  soex  7925  f1oweALT  7979  fo1stres  8022  fo2ndres  8023  ecdmn0  8776  fsetprcnex  8884  map0g  8906  ixpn0  8952  resixpfo  8958  domdifsn  9076  xpdom3  9092  fodomr  9150  mapdom3  9171  0sdom1dom  9256  unblem2  9311  fodomfir  9350  marypha1lem  9455  brwdom2  9595  unxpwdom2  9610  ixpiunwdom  9612  zfreg  9617  epfrs  9753  frmin  9771  scott0  9908  cplem1  9911  fseqen  10049  finacn  10072  iunfictbso  10136  aceq2  10141  dfac3  10143  dfac9  10159  kmlem6  10178  kmlem8  10180  infpss  10238  fin23lem7  10338  enfin2i  10343  fin23lem21  10361  fin23lem31  10365  isf32lem9  10383  isf34lem4  10399  axdc2lem  10470  axdc3lem4  10475  ac6c4  10503  ac9  10505  ac6s4  10512  ac9s  10515  ttukeyg  10539  fpwwe2lem11  10663  wun0  10740  tsk0  10785  gruina  10840  genpn0  11025  prlem934  11055  ltaddpr  11056  ltexprlem1  11058  prlem936  11069  reclem2pr  11070  suplem1pr  11074  supsr  11134  axpre-sup  11191  dedekind  11406  dedekindle  11407  negn0  11674  infm3  12209  supaddc  12217  supadd  12218  supmul1  12219  supmullem2  12221  supmul  12222  zsupss  12961  xrsupsslem  13331  xrinfmsslem  13332  supxrre  13351  infxrre  13360  ixxub  13390  ixxlb  13391  ioorebas  13473  fzn0  13560  fzon0  13699  hashgt0elexb  14423  swrdcl  14665  pfxcl  14697  maxprmfct  16728  4sqlem12  16976  vdwmc  16998  ramz  17045  ramub1  17048  mreiincl  17610  mremre  17618  mreexexlem4d  17661  iscatd2  17695  catcone0  17701  cic  17814  drsdirfi  18321  mgmpropd  18633  opifismgm  18641  dfgrp3lem  19025  dfgrp3e  19027  issubg2  19128  subgint  19137  giclcl  19260  gicrcl  19261  gicsym  19262  gictr  19263  gicen  19265  gicsubgen  19266  cntzssv  19315  symggen  19456  psgnunilem3  19482  sylow1lem4  19587  odcau  19590  sylow3  19619  cyggex2  19883  giccyg  19886  pgpfac1lem5  20067  brric2  20474  subrngint  20528  subrgint  20563  abvn0b  20805  lss0cl  20913  lmiclcl  21037  lmicrcl  21038  lmicsym  21039  lspsnat  21115  lspprat  21123  cnsubrg  21407  nzerooringczr  21453  cygzn  21543  lmiclbs  21811  lmisfree  21816  lmictra  21819  mpfrcl  22057  ply1frcl  22270  mdetdiaglem  22552  mdet0  22560  toponmre  23047  iunconnlem  23381  iunconn  23382  unconn  23383  clsconn  23384  2ndcdisj  23410  2ndcsep  23413  1stcelcls  23415  locfincmp  23480  comppfsc  23486  txcls  23558  hmphsym  23736  hmphtr  23737  hmphen  23739  haushmphlem  23741  cmphmph  23742  connhmph  23743  reghmph  23747  nrmhmph  23748  hmphdis  23750  hmphen2  23753  fbdmn0  23788  isfbas2  23789  fbssint  23792  trfbas2  23797  filtop  23809  isfil2  23810  elfg  23825  fgcl  23832  filssufilg  23865  uffix2  23878  ufildom1  23880  hauspwpwf1  23941  hausflf2  23952  alexsubALTlem2  24002  ptcmplem2  24007  cnextf  24020  tgptsmscld  24105  ustfilxp  24167  xbln0  24369  lpbl  24460  met2ndci  24479  metustfbas  24514  restmetu  24527  reconn  24786  opnreen  24789  metdsre  24811  phtpcer  24963  phtpc01  24964  phtpcco2  24968  pcohtpy  24989  cfilfcls  25244  cmetcaulem  25258  cmetcau  25259  bcthlem5  25298  ovolicc2lem2  25489  ovolicc2lem5  25492  ioorcl2  25543  ioorinv2  25546  itg11  25662  dvlip  25968  dvne0  25986  fta1g  26145  plyssc  26175  fta1  26286  vieta1lem2  26289  nocvxmin  27759  sslttr  27788  sltlpss  27881  lrrecfr  27912  hpgerlem  28709  axcontlem4  28912  axcontlem10  28918  upgrex  29037  fusgrn0degnn0  29445  uhgrvd00  29480  wspthsnonn0vne  29865  eulerpath  30188  frgrwopreglem2  30260  ubthlem1  30817  shintcli  31276  n0limd  32419  2ndimaxp  32591  fpwrelmapffslem  32678  qsxpid  33325  qsidomlem2  33416  qsdrng  33460  1arithidom  33500  dimcl  33588  lmimdim  33589  lmicdim  33590  lvecdim0i  33591  lvecdim0  33592  lssdimle  33593  dimpropd  33594  dimkerim  33613  fedgmul  33617  extdg1id  33653  fmcncfil  33889  insiga  34097  unelldsys  34118  bnj1189  34982  bnj1279  34991  pconnconn  35195  txsconn  35205  cvmsss2  35238  cvmopnlem  35242  cvmfolem  35243  cvmliftmolem2  35246  cvmlift2lem10  35276  cvmliftpht  35282  cvmlift3lem8  35290  eldm3  35720  fundmpss  35726  elima4  35735  neibastop1  36319  neibastop2lem  36320  neibastop2  36321  fnemeet2  36327  fnejoin2  36329  neifg  36331  tailfb  36337  filnetlem3  36340  bj-n0i  36911  bj-rest10  37048  bj-restn0  37050  poimirlem30  37616  itg2addnclem2  37638  prdsbnd2  37761  heibor1lem  37775  bfp  37790  divrngidl  37994  rnxrn  38358  trcoss2  38444  atex  39367  llnn0  39477  lplnn0N  39508  lvoln0N  39552  pmapglb2N  39732  pmapglb2xN  39733  elpaddn0  39761  osumcllem8N  39924  pexmidlem5N  39935  diaglbN  41016  diaintclN  41019  dibglbN  41127  dibintclN  41128  dihglblem2aN  41254  dihglblem5  41259  dihglbcpreN  41261  dihintcl  41305  unitscyglem5  42159  ricsym  42492  rictr  42493  riccrng1  42494  ricdrng1  42501  rencldnfilem  42794  kelac1  43038  lnmlmic  43063  gicabl  43074  neik0pk1imk0  44022  ntrneineine0lem  44058  scotteld  44222  onfrALT  44526  onfrALTVD  44868  iunconnlem2  44912  relpfrlem  44931  dfac5prim  44964  snelmap  45044  eliin2f  45066  disjinfi  45154  mapss2  45167  difmap  45169  infrpge  45319  infxrlesupxr  45404  inficc  45504  fsumnncl  45544  ellimciota  45586  islpcn  45611  lptre2pt  45612  stoweidlem35  46007  fourierdlem31  46110  fourier2  46199  qndenserrnbllem  46266  qndenserrnopn  46270  qndenserrn  46271  intsaluni  46301  sge0cl  46353  ovn0lem  46537  ovnsubaddlem2  46543  hoidmvval0b  46562  hspdifhsp  46588  fsetprcnexALT  47032  uniimaelsetpreimafv  47341  imasetpreimafvbijlemfv1  47348  dfgric2  47842  gricuspgr  47845  gricsym  47848  grictr  47850  gricen  47852  dfgrlic2  47926  dfgrlic3  47928  grlicen  47935  gricgrlic  47936  usgrexmpl12ngric  47955  usgrexmpl12ngrlic  47956  opmpoismgm  48041  neircl  48762  thincn0eu  49058  thinccic  49096  termcterm2  49127  eufunc  49133  euendfunc  49137  diag1f1o  49145  diag2f1o  49148  prstchom2ALT  49169  alscn0d  49322