Theorem n0 4306

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2925  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-ne 2926  df-dif 3908  df-nul 4287

This theorem is referenced by:  reximdva0  4308  rspn0  4309  n0rex  4310  n0moeu  4312  eqeuel  4318  ndisj  4323  pssnel  4424  r19.2z  4448  r19.2zb  4449  r19.3rz  4450  uniintsn  4938  iunn0  5019  trintss  5220  intex  5286  notzfaus  5305  reusv2lem1  5340  nnullss  5409  exss  5410  opabn0  5500  wefrc  5617  wereu2  5620  dmxp  5875  xpnz  6112  dmsnn0  6160  unixp0  6235  xpco  6241  frpomin  6292  onfr  6350  iotanul2  6459  fveqdmss  7016  eldmrexrnb  7030  isofrlem  7281  limuni3  7792  soex  7861  f1oweALT  7914  fo1stres  7957  fo2ndres  7958  ecdmn0  8684  fsetprcnex  8796  map0g  8818  ixpn0  8864  resixpfo  8870  domdifsn  8984  xpdom3  8999  fodomr  9052  mapdom3  9073  0sdom1dom  9145  unblem2  9198  fodomfir  9237  marypha1lem  9342  brwdom2  9484  unxpwdom2  9499  ixpiunwdom  9501  zfreg  9507  epfrs  9646  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  10554  wun0  10631  tsk0  10676  gruina  10731  genpn0  10916  prlem934  10946  ltaddpr  10947  ltexprlem1  10949  prlem936  10960  reclem2pr  10961  suplem1pr  10965  supsr  11025  axpre-sup  11082  dedekind  11297  dedekindle  11298  negn0  11567  infm3  12102  supaddc  12110  supadd  12111  supmul1  12112  supmullem2  12114  supmul  12115  zsupss  12856  xrsupsslem  13227  xrinfmsslem  13228  supxrre  13247  infxrre  13257  ixxub  13287  ixxlb  13288  ioorebas  13372  fzn0  13459  fzon0  13598  hashgt0elexb  14327  swrdcl  14570  pfxcl  14602  maxprmfct  16638  4sqlem12  16886  vdwmc  16908  ramz  16955  ramub1  16958  mreiincl  17516  mremre  17524  mreexexlem4d  17571  iscatd2  17605  catcone0  17611  cic  17724  drsdirfi  18229  mgmpropd  18543  opifismgm  18551  dfgrp3lem  18935  dfgrp3e  18937  issubg2  19038  subgint  19047  giclcl  19170  gicrcl  19171  gicsym  19172  gictr  19173  gicen  19175  gicsubgen  19176  cntzssv  19225  symggen  19367  psgnunilem3  19393  sylow1lem4  19498  odcau  19501  sylow3  19530  cyggex2  19794  giccyg  19797  pgpfac1lem5  19978  brric2  20409  subrngint  20463  subrgint  20498  abvn0b  20739  lss0cl  20868  lmiclcl  20992  lmicrcl  20993  lmicsym  20994  lspsnat  21070  lspprat  21078  cnsubrg  21352  nzerooringczr  21405  cygzn  21495  lmiclbs  21762  lmisfree  21767  lmictra  21770  mpfrcl  22008  ply1frcl  22221  mdetdiaglem  22501  mdet0  22509  toponmre  22996  iunconnlem  23330  iunconn  23331  unconn  23332  clsconn  23333  2ndcdisj  23359  2ndcsep  23362  1stcelcls  23364  locfincmp  23429  comppfsc  23435  txcls  23507  hmphsym  23685  hmphtr  23686  hmphen  23688  haushmphlem  23690  cmphmph  23691  connhmph  23692  reghmph  23696  nrmhmph  23697  hmphdis  23699  hmphen2  23702  fbdmn0  23737  isfbas2  23738  fbssint  23741  trfbas2  23746  filtop  23758  isfil2  23759  elfg  23774  fgcl  23781  filssufilg  23814  uffix2  23827  ufildom1  23829  hauspwpwf1  23890  hausflf2  23901  alexsubALTlem2  23951  ptcmplem2  23956  cnextf  23969  tgptsmscld  24054  ustfilxp  24116  xbln0  24318  lpbl  24407  met2ndci  24426  metustfbas  24461  restmetu  24474  reconn  24733  opnreen  24736  metdsre  24758  phtpcer  24910  phtpc01  24911  phtpcco2  24915  pcohtpy  24936  cfilfcls  25190  cmetcaulem  25204  cmetcau  25205  bcthlem5  25244  ovolicc2lem2  25435  ovolicc2lem5  25438  ioorcl2  25489  ioorinv2  25492  itg11  25608  dvlip  25914  dvne0  25932  fta1g  26091  plyssc  26121  fta1  26232  vieta1lem2  26235  nobdaymin  27705  sslttr  27736  sltlpss  27840  lrrecfr  27873  onscutlt  28188  hpgerlem  28728  axcontlem4  28930  axcontlem10  28936  upgrex  29055  fusgrn0degnn0  29463  uhgrvd00  29498  wspthsnonn0vne  29880  eulerpath  30203  frgrwopreglem2  30275  ubthlem1  30832  shintcli  31291  n0limd  32434  2ndimaxp  32603  fpwrelmapffslem  32688  qsxpid  33309  qsidomlem2  33400  qsdrng  33444  1arithidom  33484  dimcl  33574  lmimdim  33575  lmicdim  33576  lvecdim0i  33577  lvecdim0  33578  lssdimle  33579  dimpropd  33580  dimkerim  33599  fedgmul  33603  extdg1id  33637  fmcncfil  33897  insiga  34103  unelldsys  34124  bnj1189  34975  bnj1279  34984  axregszf  35063  pconnconn  35203  txsconn  35213  cvmsss2  35246  cvmopnlem  35250  cvmfolem  35251  cvmliftmolem2  35254  cvmlift2lem10  35284  cvmliftpht  35290  cvmlift3lem8  35298  eldm3  35733  fundmpss  35739  elima4  35748  neibastop1  36332  neibastop2lem  36333  neibastop2  36334  fnemeet2  36340  fnejoin2  36342  neifg  36344  tailfb  36350  filnetlem3  36353  bj-n0i  36924  bj-rest10  37061  bj-restn0  37063  poimirlem30  37629  itg2addnclem2  37651  prdsbnd2  37774  heibor1lem  37788  bfp  37803  divrngidl  38007  eldmres3  38250  rnxrn  38369  eldmxrncnvepres2  38382  trcoss2  38460  atex  39385  llnn0  39495  lplnn0N  39526  lvoln0N  39570  pmapglb2N  39750  pmapglb2xN  39751  elpaddn0  39779  osumcllem8N  39942  pexmidlem5N  39953  diaglbN  41034  diaintclN  41037  dibglbN  41145  dibintclN  41146  dihglblem2aN  41272  dihglblem5  41277  dihglbcpreN  41279  dihintcl  41323  unitscyglem5  42172  ricsym  42492  rictr  42493  riccrng1  42494  ricdrng1  42501  rencldnfilem  42793  kelac1  43036  lnmlmic  43061  gicabl  43072  neik0pk1imk0  44020  ntrneineine0lem  44056  scotteld  44219  onfrALT  44523  onfrALTVD  44864  iunconnlem2  44908  relpfrlem  44927  dfac5prim  44964  permac8prim  44988  snelmap  45060  eliin2f  45082  disjinfi  45170  mapss2  45183  difmap  45185  infrpge  45331  infxrlesupxr  45416  inficc  45516  fsumnncl  45554  ellimciota  45596  islpcn  45621  lptre2pt  45622  stoweidlem35  46017  fourierdlem31  46120  fourier2  46209  qndenserrnbllem  46276  qndenserrnopn  46280  qndenserrn  46281  intsaluni  46311  sge0cl  46363  ovn0lem  46547  ovnsubaddlem2  46553  hoidmvval0b  46572  hspdifhsp  46598  fsetprcnexALT  47047  uniimaelsetpreimafv  47381  imasetpreimafvbijlemfv1  47388  dfgric2  47900  gricuspgr  47903  gricsym  47906  grictr  47908  gricen  47910  dfgrlic2  47993  dfgrlic3  47995  grlicen  48002  gricgrlic  48003  usgrexmpl12ngric  48023  usgrexmpl12ngrlic  48024  opmpoismgm  48152  neircl  48890  sectrcl  49008  invrcl  49010  isorcl  49019  iinfssc  49043  iinfsubc  49044  imaid  49140  thincn0eu  49417  thinccic  49457  termcterm2  49500  eufunc  49508  euendfunc  49512  diag1f1o  49520  diag2f1o  49523  prstchom2ALT  49550  rellan  49609  relran  49610  alscn0d  49781