Theorem n0 4305

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ≠ wne 2932  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-ne 2933  df-dif 3904  df-nul 4286

This theorem is referenced by:  reximdva0  4307  rspn0  4308  n0rex  4309  n0moeu  4311  eqeuel  4317  ndisj  4322  pssnel  4423  r19.2z  4452  r19.3rz  4454  uniintsn  4940  iunn0  5022  trintss  5223  intex  5289  notzfaus  5308  reusv2lem1  5343  nnullss  5410  exss  5411  opabn0  5501  wefrc  5618  wereu2  5621  dmxp  5878  xpnz  6117  dmsnn0  6165  unixp0  6241  xpco  6247  frpomin  6298  onfr  6356  iotanul2  6465  fveqdmss  7023  eldmrexrnb  7037  isofrlem  7286  limuni3  7794  soex  7863  f1oweALT  7916  fo1stres  7959  fo2ndres  7960  ecdmn0  8687  fsetprcnex  8799  map0g  8822  ixpn0  8868  resixpfo  8874  domdifsn  8988  xpdom3  9003  fodomr  9056  mapdom3  9077  0sdom1dom  9146  unblem2  9193  fodomfir  9228  marypha1lem  9336  brwdom2  9478  unxpwdom2  9493  ixpiunwdom  9495  zfreg  9501  epfrs  9640  frmin  9661  scott0  9798  cplem1  9801  fseqen  9937  finacn  9960  iunfictbso  10024  aceq2  10029  dfac3  10031  dfac9  10047  kmlem6  10066  kmlem8  10068  infpss  10126  fin23lem7  10226  enfin2i  10231  fin23lem21  10249  fin23lem31  10253  isf32lem9  10271  isf34lem4  10287  axdc2lem  10358  axdc3lem4  10363  ac6c4  10391  ac9  10393  ac6s4  10400  ac9s  10403  ttukeyg  10427  fpwwe2lem11  10552  wun0  10629  tsk0  10674  gruina  10729  genpn0  10914  prlem934  10944  ltaddpr  10945  ltexprlem1  10947  prlem936  10958  reclem2pr  10959  suplem1pr  10963  supsr  11023  axpre-sup  11080  dedekind  11296  dedekindle  11297  negn0  11566  infm3  12101  supaddc  12109  supadd  12110  supmul1  12111  supmullem2  12113  supmul  12114  zsupss  12850  xrsupsslem  13222  xrinfmsslem  13223  supxrre  13242  infxrre  13252  ixxub  13282  ixxlb  13283  ioorebas  13367  fzn0  13454  fzon0  13593  hashgt0elexb  14325  swrdcl  14569  pfxcl  14601  maxprmfct  16636  4sqlem12  16884  vdwmc  16906  ramz  16953  ramub1  16956  mreiincl  17515  mremre  17523  mreexexlem4d  17570  iscatd2  17604  catcone0  17610  cic  17723  drsdirfi  18228  mgmpropd  18576  opifismgm  18584  dfgrp3lem  18968  dfgrp3e  18970  issubg2  19071  subgint  19080  giclcl  19202  gicrcl  19203  gicsym  19204  gictr  19205  gicen  19207  gicsubgen  19208  cntzssv  19257  symggen  19399  psgnunilem3  19425  sylow1lem4  19530  odcau  19533  sylow3  19562  cyggex2  19826  giccyg  19829  pgpfac1lem5  20010  brric2  20439  subrngint  20493  subrgint  20528  abvn0b  20769  lss0cl  20898  lmiclcl  21022  lmicrcl  21023  lmicsym  21024  lspsnat  21100  lspprat  21108  cnsubrg  21382  nzerooringczr  21435  cygzn  21525  lmiclbs  21792  lmisfree  21797  lmictra  21800  mpfrcl  22040  ply1frcl  22262  mdetdiaglem  22542  mdet0  22550  toponmre  23037  iunconnlem  23371  iunconn  23372  unconn  23373  clsconn  23374  2ndcdisj  23400  2ndcsep  23403  1stcelcls  23405  locfincmp  23470  comppfsc  23476  txcls  23548  hmphsym  23726  hmphtr  23727  hmphen  23729  haushmphlem  23731  cmphmph  23732  connhmph  23733  reghmph  23737  nrmhmph  23738  hmphdis  23740  hmphen2  23743  fbdmn0  23778  isfbas2  23779  fbssint  23782  trfbas2  23787  filtop  23799  isfil2  23800  elfg  23815  fgcl  23822  filssufilg  23855  uffix2  23868  ufildom1  23870  hauspwpwf1  23931  hausflf2  23942  alexsubALTlem2  23992  ptcmplem2  23997  cnextf  24010  tgptsmscld  24095  ustfilxp  24157  xbln0  24358  lpbl  24447  met2ndci  24466  metustfbas  24501  restmetu  24514  reconn  24773  opnreen  24776  metdsre  24798  phtpcer  24950  phtpc01  24951  phtpcco2  24955  pcohtpy  24976  cfilfcls  25230  cmetcaulem  25244  cmetcau  25245  bcthlem5  25284  ovolicc2lem2  25475  ovolicc2lem5  25478  ioorcl2  25529  ioorinv2  25532  itg11  25648  dvlip  25954  dvne0  25972  fta1g  26131  plyssc  26161  fta1  26272  vieta1lem2  26275  nobdaymin  27749  sltstr  27783  ltslpss  27904  lrrecfr  27939  oncutlt  28260  hpgerlem  28837  axcontlem4  29040  axcontlem10  29046  upgrex  29165  fusgrn0degnn0  29573  uhgrvd00  29608  wspthsnonn0vne  29990  eulerpath  30316  frgrwopreglem2  30388  ubthlem1  30945  shintcli  31404  n0limd  32546  2ndimaxp  32724  fpwrelmapffslem  32811  qsxpid  33443  qsidomlem2  33534  qsdrng  33578  1arithidom  33618  dimcl  33759  lmimdim  33760  lmicdim  33761  lvecdim0i  33762  lvecdim0  33763  lssdimle  33764  dimpropd  33765  dimkerim  33784  fedgmul  33788  extdg1id  33823  fmcncfil  34088  insiga  34294  unelldsys  34315  bnj1189  35165  bnj1279  35174  axregszf  35285  pconnconn  35425  txsconn  35435  cvmsss2  35468  cvmopnlem  35472  cvmfolem  35473  cvmliftmolem2  35476  cvmlift2lem10  35506  cvmliftpht  35512  cvmlift3lem8  35520  eldm3  35955  fundmpss  35961  elima4  35970  neibastop1  36553  neibastop2lem  36554  neibastop2  36555  fnemeet2  36561  fnejoin2  36563  neifg  36565  tailfb  36571  filnetlem3  36574  bj-n0i  37152  bj-rest10  37289  bj-restn0  37291  poimirlem30  37847  itg2addnclem2  37869  prdsbnd2  37992  heibor1lem  38006  bfp  38021  divrngidl  38225  eldmres3  38472  rnxrn  38602  eldmxrncnvepres2  38616  trcoss2  38743  atex  39662  llnn0  39772  lplnn0N  39803  lvoln0N  39847  pmapglb2N  40027  pmapglb2xN  40028  elpaddn0  40056  osumcllem8N  40219  pexmidlem5N  40230  diaglbN  41311  diaintclN  41314  dibglbN  41422  dibintclN  41423  dihglblem2aN  41549  dihglblem5  41554  dihglbcpreN  41556  dihintcl  41600  unitscyglem5  42449  ricsym  42770  rictr  42771  riccrng1  42772  ricdrng1  42779  rencldnfilem  43058  kelac1  43301  lnmlmic  43326  gicabl  43337  neik0pk1imk0  44284  ntrneineine0lem  44320  scotteld  44483  onfrALT  44786  onfrALTVD  45127  iunconnlem2  45171  relpfrlem  45190  dfac5prim  45227  permac8prim  45251  snelmap  45323  eliin2f  45344  disjinfi  45432  mapss2  45445  difmap  45447  infrpge  45592  infxrlesupxr  45676  inficc  45776  fsumnncl  45814  ellimciota  45856  islpcn  45879  lptre2pt  45880  stoweidlem35  46275  fourierdlem31  46378  fourier2  46467  qndenserrnbllem  46534  qndenserrnopn  46538  qndenserrn  46539  intsaluni  46569  sge0cl  46621  ovn0lem  46805  ovnsubaddlem2  46811  hoidmvval0b  46830  hspdifhsp  46856  fsetprcnexALT  47304  uniimaelsetpreimafv  47638  imasetpreimafvbijlemfv1  47645  dfgric2  48157  gricuspgr  48160  gricsym  48163  grictr  48165  gricen  48167  dfgrlic2  48250  dfgrlic3  48252  grlicen  48259  gricgrlic  48260  usgrexmpl12ngric  48280  usgrexmpl12ngrlic  48281  opmpoismgm  48409  neircl  49146  sectrcl  49263  invrcl  49265  isorcl  49274  iinfssc  49298  iinfsubc  49299  imaid  49395  thincn0eu  49672  thinccic  49712  termcterm2  49755  eufunc  49763  euendfunc  49767  diag1f1o  49775  diag2f1o  49778  prstchom2ALT  49805  rellan  49864  relran  49865  alscn0d  50036