Theorem n0 4297

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 2942	. 2 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
2		neq0 4296	. 2 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
3	1, 2	bitri 275	1 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ≠ wne 2941  ∅c0 4273

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-ne 2942  df-dif 3904  df-nul 4274

This theorem is referenced by:  reximdva0  4302  rspn0  4303  rspn0OLD  4304  n0rex  4305  n0moeu  4307  eqeuel  4313  ndisj  4318  pssnel  4421  r19.2z  4443  r19.2zb  4444  r19.3rz  4445  uniintsn  4939  iunn0  5018  trintss  5232  intex  5285  notzfaus  5309  reusv2lem1  5345  nnullss  5411  exss  5412  opabn0  5501  wefrc  5618  wereu2  5621  dmxp  5874  xpnz  6101  dmsnn0  6149  unixp0  6225  xpco  6231  frpomin  6283  onfr  6345  iotanul2  6453  fveqdmss  7016  eldmrexrnb  7028  isofrlem  7271  limuni3  7770  soex  7840  f1oweALT  7887  fo1stres  7929  fo2ndres  7930  ecdmn0  8620  fsetprcnex  8725  map0g  8747  ixpn0  8793  resixpfo  8799  domdifsn  8923  xpdom3  8939  fodomr  8997  mapdom3  9018  0sdom1dom  9107  findcard2OLD  9153  unblem2  9165  marypha1lem  9294  brwdom2  9434  unxpwdom2  9449  ixpiunwdom  9451  zfreg  9456  epfrs  9592  frmin  9610  scott0  9747  cplem1  9750  fseqen  9888  finacn  9911  iunfictbso  9975  aceq2  9980  dfac3  9982  dfac9  9997  kmlem6  10016  kmlem8  10018  infpss  10078  fin23lem7  10177  enfin2i  10182  fin23lem21  10200  fin23lem31  10204  isf32lem9  10222  isf34lem4  10238  axdc2lem  10309  axdc3lem4  10314  ac6c4  10342  ac9  10344  ac6s4  10351  ac9s  10354  ttukeyg  10378  fpwwe2lem11  10502  wun0  10579  tsk0  10624  gruina  10679  genpn0  10864  prlem934  10894  ltaddpr  10895  ltexprlem1  10897  prlem936  10908  reclem2pr  10909  suplem1pr  10913  supsr  10973  axpre-sup  11030  dedekind  11243  dedekindle  11244  negn0  11509  infm3  12039  supaddc  12047  supadd  12048  supmul1  12049  supmullem2  12051  supmul  12052  zsupss  12782  xrsupsslem  13146  xrinfmsslem  13147  supxrre  13166  infxrre  13175  ixxub  13205  ixxlb  13206  ioorebas  13288  fzn0  13375  fzon0  13510  hashgt0elexb  14221  swrdcl  14456  pfxcl  14488  maxprmfct  16511  4sqlem12  16754  vdwmc  16776  ramz  16823  ramub1  16826  mreiincl  17402  mremre  17410  mreexexlem4d  17453  iscatd2  17487  catcone0  17493  cic  17608  drsdirfi  18120  opifismgm  18440  dfgrp3lem  18769  dfgrp3e  18771  issubg2  18866  subgint  18875  giclcl  18984  gicrcl  18985  gicsym  18986  gictr  18987  gicen  18989  gicsubgen  18990  cntzssv  19030  symggen  19174  psgnunilem3  19200  sylow1lem4  19302  odcau  19305  sylow3  19334  cyggex2  19592  giccyg  19595  pgpfac1lem5  19776  brric2  20086  subrgint  20150  lss0cl  20313  lmiclcl  20437  lmicrcl  20438  lmicsym  20439  lspsnat  20512  lspprat  20520  abvn0b  20678  cnsubrg  20763  cygzn  20883  lmiclbs  21149  lmisfree  21154  lmictra  21157  mpfrcl  21400  ply1frcl  21589  mdetdiaglem  21852  mdet0  21860  toponmre  22349  iunconnlem  22683  iunconn  22684  unconn  22685  clsconn  22686  2ndcdisj  22712  2ndcsep  22715  1stcelcls  22717  locfincmp  22782  comppfsc  22788  txcls  22860  hmphsym  23038  hmphtr  23039  hmphen  23041  haushmphlem  23043  cmphmph  23044  connhmph  23045  reghmph  23049  nrmhmph  23050  hmphdis  23052  hmphen2  23055  fbdmn0  23090  isfbas2  23091  fbssint  23094  trfbas2  23099  filtop  23111  isfil2  23112  elfg  23127  fgcl  23134  filssufilg  23167  uffix2  23180  ufildom1  23182  hauspwpwf1  23243  hausflf2  23254  alexsubALTlem2  23304  ptcmplem2  23309  cnextf  23322  tgptsmscld  23407  ustfilxp  23469  xbln0  23672  lpbl  23764  met2ndci  23783  metustfbas  23818  restmetu  23831  reconn  24096  opnreen  24099  metdsre  24121  phtpcer  24263  phtpc01  24264  phtpcco2  24267  pcohtpy  24288  cfilfcls  24543  cmetcaulem  24557  cmetcau  24558  bcthlem5  24597  ovolicc2lem2  24787  ovolicc2lem5  24790  ioorcl2  24841  ioorinv2  24844  itg11  24960  dvlip  25262  dvne0  25280  fta1g  25437  plyssc  25466  fta1  25573  vieta1lem2  25576  nocvxmin  27023  sslttr  27051  hpgerlem  27414  axcontlem4  27623  axcontlem10  27629  upgrex  27750  fusgrn0degnn0  28154  uhgrvd00  28189  wspthsnonn0vne  28569  eulerpath  28892  frgrwopreglem2  28964  ubthlem1  29519  shintcli  29978  2ndimaxp  31269  fpwrelmapffslem  31352  qsxpid  31852  qsidomlem2  31924  dimcl  31984  lvecdim0i  31985  lvecdim0  31986  lssdimle  31987  dimpropd  31988  dimkerim  32004  fedgmul  32008  extdg1id  32034  fmcncfil  32177  insiga  32401  unelldsys  32422  bnj1189  33286  bnj1279  33295  pconnconn  33490  txsconn  33500  cvmsss2  33533  cvmopnlem  33537  cvmfolem  33538  cvmliftmolem2  33541  cvmlift2lem10  33571  cvmliftpht  33577  cvmlift3lem8  33585  eldm3  34017  fundmpss  34024  elima4  34033  sltlpss  34195  lrrecfr  34208  neibastop1  34685  neibastop2lem  34686  neibastop2  34687  fnemeet2  34693  fnejoin2  34695  neifg  34697  tailfb  34703  filnetlem3  34706  bj-n0i  35276  bj-rest10  35413  bj-restn0  35415  poimirlem30  35963  itg2addnclem2  35985  prdsbnd2  36109  heibor1lem  36123  bfp  36138  divrngidl  36342  rnxrn  36716  trcoss2  36802  atex  37725  llnn0  37835  lplnn0N  37866  lvoln0N  37910  pmapglb2N  38090  pmapglb2xN  38091  elpaddn0  38119  osumcllem8N  38282  pexmidlem5N  38293  diaglbN  39374  diaintclN  39377  dibglbN  39485  dibintclN  39486  dihglblem2aN  39612  dihglblem5  39617  dihglbcpreN  39619  dihintcl  39663  ricsym  40555  rictr  40556  riccrng1  40557  rencldnfilem  40955  kelac1  41202  lnmlmic  41227  gicabl  41238  neik0pk1imk0  42030  ntrneineine0lem  42066  scotteld  42237  onfrALT  42542  onfrALTVD  42884  iunconnlem2  42928  snelmap  43004  eliin2f  43026  disjinfi  43110  mapss2  43124  difmap  43126  infrpge  43277  infxrlesupxr  43363  inficc  43460  fsumnncl  43501  ellimciota  43543  islpcn  43568  lptre2pt  43569  stoweidlem35  43964  fourierdlem31  44067  fourier2  44156  qndenserrnbllem  44223  qndenserrnopn  44227  qndenserrn  44228  intsaluni  44256  sge0cl  44308  ovn0lem  44492  ovnsubaddlem2  44498  hoidmvval0b  44517  hspdifhsp  44543  fsetprcnexALT  44974  uniimaelsetpreimafv  45266  imasetpreimafvbijlemfv1  45273  mgmpropd  45747  opmpoismgm  45779  nzerooringczr  46048  neircl  46616  thincn0eu  46731  thinccic  46760  prstchom2ALT  46778  alscn0d  46917