Theorem n0 4302

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 2182. (Revised by GG, 28-Jun-2024.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

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

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 2705

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 2712  df-cleq 2725  df-ne 2930  df-dif 3901  df-nul 4283

This theorem is referenced by:  reximdva0  4304  rspn0  4305  n0rex  4306  n0moeu  4308  eqeuel  4314  ndisj  4319  pssnel  4420  r19.2z  4444  r19.2zb  4445  r19.3rz  4446  uniintsn  4935  iunn0  5017  trintss  5218  intex  5284  notzfaus  5303  reusv2lem1  5338  nnullss  5405  exss  5406  opabn0  5496  wefrc  5613  wereu2  5616  dmxp  5873  xpnz  6111  dmsnn0  6159  unixp0  6235  xpco  6241  frpomin  6292  onfr  6350  iotanul2  6459  fveqdmss  7017  eldmrexrnb  7031  isofrlem  7280  limuni3  7788  soex  7857  f1oweALT  7910  fo1stres  7953  fo2ndres  7954  ecdmn0  8680  fsetprcnex  8792  map0g  8814  ixpn0  8860  resixpfo  8866  domdifsn  8980  xpdom3  8995  fodomr  9048  mapdom3  9069  0sdom1dom  9137  unblem2  9184  fodomfir  9219  marypha1lem  9324  brwdom2  9466  unxpwdom2  9481  ixpiunwdom  9483  zfreg  9489  epfrs  9628  frmin  9649  scott0  9786  cplem1  9789  fseqen  9925  finacn  9948  iunfictbso  10012  aceq2  10017  dfac3  10019  dfac9  10035  kmlem6  10054  kmlem8  10056  infpss  10114  fin23lem7  10214  enfin2i  10219  fin23lem21  10237  fin23lem31  10241  isf32lem9  10259  isf34lem4  10275  axdc2lem  10346  axdc3lem4  10351  ac6c4  10379  ac9  10381  ac6s4  10388  ac9s  10391  ttukeyg  10415  fpwwe2lem11  10539  wun0  10616  tsk0  10661  gruina  10716  genpn0  10901  prlem934  10931  ltaddpr  10932  ltexprlem1  10934  prlem936  10945  reclem2pr  10946  suplem1pr  10950  supsr  11010  axpre-sup  11067  dedekind  11283  dedekindle  11284  negn0  11553  infm3  12088  supaddc  12096  supadd  12097  supmul1  12098  supmullem2  12100  supmul  12101  zsupss  12837  xrsupsslem  13208  xrinfmsslem  13209  supxrre  13228  infxrre  13238  ixxub  13268  ixxlb  13269  ioorebas  13353  fzn0  13440  fzon0  13579  hashgt0elexb  14311  swrdcl  14555  pfxcl  14587  maxprmfct  16622  4sqlem12  16870  vdwmc  16892  ramz  16939  ramub1  16942  mreiincl  17500  mremre  17508  mreexexlem4d  17555  iscatd2  17589  catcone0  17595  cic  17708  drsdirfi  18213  mgmpropd  18561  opifismgm  18569  dfgrp3lem  18953  dfgrp3e  18955  issubg2  19056  subgint  19065  giclcl  19187  gicrcl  19188  gicsym  19189  gictr  19190  gicen  19192  gicsubgen  19193  cntzssv  19242  symggen  19384  psgnunilem3  19410  sylow1lem4  19515  odcau  19518  sylow3  19547  cyggex2  19811  giccyg  19814  pgpfac1lem5  19995  brric2  20423  subrngint  20477  subrgint  20512  abvn0b  20753  lss0cl  20882  lmiclcl  21006  lmicrcl  21007  lmicsym  21008  lspsnat  21084  lspprat  21092  cnsubrg  21366  nzerooringczr  21419  cygzn  21509  lmiclbs  21776  lmisfree  21781  lmictra  21784  mpfrcl  22021  ply1frcl  22234  mdetdiaglem  22514  mdet0  22522  toponmre  23009  iunconnlem  23343  iunconn  23344  unconn  23345  clsconn  23346  2ndcdisj  23372  2ndcsep  23375  1stcelcls  23377  locfincmp  23442  comppfsc  23448  txcls  23520  hmphsym  23698  hmphtr  23699  hmphen  23701  haushmphlem  23703  cmphmph  23704  connhmph  23705  reghmph  23709  nrmhmph  23710  hmphdis  23712  hmphen2  23715  fbdmn0  23750  isfbas2  23751  fbssint  23754  trfbas2  23759  filtop  23771  isfil2  23772  elfg  23787  fgcl  23794  filssufilg  23827  uffix2  23840  ufildom1  23842  hauspwpwf1  23903  hausflf2  23914  alexsubALTlem2  23964  ptcmplem2  23969  cnextf  23982  tgptsmscld  24067  ustfilxp  24129  xbln0  24330  lpbl  24419  met2ndci  24438  metustfbas  24473  restmetu  24486  reconn  24745  opnreen  24748  metdsre  24770  phtpcer  24922  phtpc01  24923  phtpcco2  24927  pcohtpy  24948  cfilfcls  25202  cmetcaulem  25216  cmetcau  25217  bcthlem5  25256  ovolicc2lem2  25447  ovolicc2lem5  25450  ioorcl2  25501  ioorinv2  25504  itg11  25620  dvlip  25926  dvne0  25944  fta1g  26103  plyssc  26133  fta1  26244  vieta1lem2  26247  nobdaymin  27717  sslttr  27749  sltlpss  27854  lrrecfr  27887  onscutlt  28202  hpgerlem  28744  axcontlem4  28947  axcontlem10  28953  upgrex  29072  fusgrn0degnn0  29480  uhgrvd00  29515  wspthsnonn0vne  29897  eulerpath  30223  frgrwopreglem2  30295  ubthlem1  30852  shintcli  31311  n0limd  32453  2ndimaxp  32630  fpwrelmapffslem  32719  qsxpid  33334  qsidomlem2  33425  qsdrng  33469  1arithidom  33509  dimcl  33636  lmimdim  33637  lmicdim  33638  lvecdim0i  33639  lvecdim0  33640  lssdimle  33641  dimpropd  33642  dimkerim  33661  fedgmul  33665  extdg1id  33700  fmcncfil  33965  insiga  34171  unelldsys  34192  bnj1189  35042  bnj1279  35051  axregszf  35148  pconnconn  35296  txsconn  35306  cvmsss2  35339  cvmopnlem  35343  cvmfolem  35344  cvmliftmolem2  35347  cvmlift2lem10  35377  cvmliftpht  35383  cvmlift3lem8  35391  eldm3  35826  fundmpss  35832  elima4  35841  neibastop1  36424  neibastop2lem  36425  neibastop2  36426  fnemeet2  36432  fnejoin2  36434  neifg  36436  tailfb  36442  filnetlem3  36445  bj-n0i  37016  bj-rest10  37153  bj-restn0  37155  poimirlem30  37711  itg2addnclem2  37733  prdsbnd2  37856  heibor1lem  37870  bfp  37885  divrngidl  38089  eldmres3  38336  rnxrn  38466  eldmxrncnvepres2  38480  trcoss2  38607  atex  39526  llnn0  39636  lplnn0N  39667  lvoln0N  39711  pmapglb2N  39891  pmapglb2xN  39892  elpaddn0  39920  osumcllem8N  40083  pexmidlem5N  40094  diaglbN  41175  diaintclN  41178  dibglbN  41286  dibintclN  41287  dihglblem2aN  41413  dihglblem5  41418  dihglbcpreN  41420  dihintcl  41464  unitscyglem5  42313  ricsym  42638  rictr  42639  riccrng1  42640  ricdrng1  42647  rencldnfilem  42938  kelac1  43181  lnmlmic  43206  gicabl  43217  neik0pk1imk0  44165  ntrneineine0lem  44201  scotteld  44364  onfrALT  44667  onfrALTVD  45008  iunconnlem2  45052  relpfrlem  45071  dfac5prim  45108  permac8prim  45132  snelmap  45204  eliin2f  45226  disjinfi  45314  mapss2  45327  difmap  45329  infrpge  45475  infxrlesupxr  45559  inficc  45659  fsumnncl  45697  ellimciota  45739  islpcn  45762  lptre2pt  45763  stoweidlem35  46158  fourierdlem31  46261  fourier2  46350  qndenserrnbllem  46417  qndenserrnopn  46421  qndenserrn  46422  intsaluni  46452  sge0cl  46504  ovn0lem  46688  ovnsubaddlem2  46694  hoidmvval0b  46713  hspdifhsp  46739  fsetprcnexALT  47187  uniimaelsetpreimafv  47521  imasetpreimafvbijlemfv1  47528  dfgric2  48040  gricuspgr  48043  gricsym  48046  grictr  48048  gricen  48050  dfgrlic2  48133  dfgrlic3  48135  grlicen  48142  gricgrlic  48143  usgrexmpl12ngric  48163  usgrexmpl12ngrlic  48164  opmpoismgm  48292  neircl  49030  sectrcl  49148  invrcl  49150  isorcl  49159  iinfssc  49183  iinfsubc  49184  imaid  49280  thincn0eu  49557  thinccic  49597  termcterm2  49640  eufunc  49648  euendfunc  49652  diag1f1o  49660  diag2f1o  49663  prstchom2ALT  49690  rellan  49749  relran  49750  alscn0d  49921