Theorem n0 4345

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 2155, ax-12 2172. (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 4344	. 2 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
3	1, 2	bitri 275	1 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1542  ∃wex 1782   ∈ wcel 2107   ≠ wne 2941  ∅c0 4321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-ne 2942  df-dif 3950  df-nul 4322

This theorem is referenced by:  reximdva0  4350  rspn0  4351  rspn0OLD  4352  n0rex  4353  n0moeu  4355  eqeuel  4361  ndisj  4366  pssnel  4469  r19.2z  4493  r19.2zb  4494  r19.3rz  4495  uniintsn  4990  iunn0  5069  trintss  5283  intex  5336  notzfaus  5360  reusv2lem1  5395  nnullss  5461  exss  5462  opabn0  5552  wefrc  5669  wereu2  5672  dmxp  5926  xpnz  6155  dmsnn0  6203  unixp0  6279  xpco  6285  frpomin  6338  onfr  6400  iotanul2  6510  fveqdmss  7076  eldmrexrnb  7089  isofrlem  7332  limuni3  7836  soex  7907  f1oweALT  7954  fo1stres  7996  fo2ndres  7997  ecdmn0  8746  fsetprcnex  8852  map0g  8874  ixpn0  8920  resixpfo  8926  domdifsn  9050  xpdom3  9066  fodomr  9124  mapdom3  9145  0sdom1dom  9234  findcard2OLD  9280  unblem2  9292  marypha1lem  9424  brwdom2  9564  unxpwdom2  9579  ixpiunwdom  9581  zfreg  9586  epfrs  9722  frmin  9740  scott0  9877  cplem1  9880  fseqen  10018  finacn  10041  iunfictbso  10105  aceq2  10110  dfac3  10112  dfac9  10127  kmlem6  10146  kmlem8  10148  infpss  10208  fin23lem7  10307  enfin2i  10312  fin23lem21  10330  fin23lem31  10334  isf32lem9  10352  isf34lem4  10368  axdc2lem  10439  axdc3lem4  10444  ac6c4  10472  ac9  10474  ac6s4  10481  ac9s  10484  ttukeyg  10508  fpwwe2lem11  10632  wun0  10709  tsk0  10754  gruina  10809  genpn0  10994  prlem934  11024  ltaddpr  11025  ltexprlem1  11027  prlem936  11038  reclem2pr  11039  suplem1pr  11043  supsr  11103  axpre-sup  11160  dedekind  11373  dedekindle  11374  negn0  11639  infm3  12169  supaddc  12177  supadd  12178  supmul1  12179  supmullem2  12181  supmul  12182  zsupss  12917  xrsupsslem  13282  xrinfmsslem  13283  supxrre  13302  infxrre  13311  ixxub  13341  ixxlb  13342  ioorebas  13424  fzn0  13511  fzon0  13646  hashgt0elexb  14358  swrdcl  14591  pfxcl  14623  maxprmfct  16642  4sqlem12  16885  vdwmc  16907  ramz  16954  ramub1  16957  mreiincl  17536  mremre  17544  mreexexlem4d  17587  iscatd2  17621  catcone0  17627  cic  17742  drsdirfi  18254  opifismgm  18574  dfgrp3lem  18917  dfgrp3e  18919  issubg2  19015  subgint  19024  giclcl  19140  gicrcl  19141  gicsym  19142  gictr  19143  gicen  19145  gicsubgen  19146  cntzssv  19186  symggen  19331  psgnunilem3  19357  sylow1lem4  19462  odcau  19465  sylow3  19494  cyggex2  19757  giccyg  19760  pgpfac1lem5  19941  brric2  20274  subrgint  20374  lss0cl  20545  lmiclcl  20669  lmicrcl  20670  lmicsym  20671  lspsnat  20746  lspprat  20754  abvn0b  20905  cnsubrg  20990  cygzn  21110  lmiclbs  21376  lmisfree  21381  lmictra  21384  mpfrcl  21630  ply1frcl  21819  mdetdiaglem  22082  mdet0  22090  toponmre  22579  iunconnlem  22913  iunconn  22914  unconn  22915  clsconn  22916  2ndcdisj  22942  2ndcsep  22945  1stcelcls  22947  locfincmp  23012  comppfsc  23018  txcls  23090  hmphsym  23268  hmphtr  23269  hmphen  23271  haushmphlem  23273  cmphmph  23274  connhmph  23275  reghmph  23279  nrmhmph  23280  hmphdis  23282  hmphen2  23285  fbdmn0  23320  isfbas2  23321  fbssint  23324  trfbas2  23329  filtop  23341  isfil2  23342  elfg  23357  fgcl  23364  filssufilg  23397  uffix2  23410  ufildom1  23412  hauspwpwf1  23473  hausflf2  23484  alexsubALTlem2  23534  ptcmplem2  23539  cnextf  23552  tgptsmscld  23637  ustfilxp  23699  xbln0  23902  lpbl  23994  met2ndci  24013  metustfbas  24048  restmetu  24061  reconn  24326  opnreen  24329  metdsre  24351  phtpcer  24493  phtpc01  24494  phtpcco2  24497  pcohtpy  24518  cfilfcls  24773  cmetcaulem  24787  cmetcau  24788  bcthlem5  24827  ovolicc2lem2  25017  ovolicc2lem5  25020  ioorcl2  25071  ioorinv2  25074  itg11  25190  dvlip  25492  dvne0  25510  fta1g  25667  plyssc  25696  fta1  25803  vieta1lem2  25806  nocvxmin  27260  sslttr  27288  sltlpss  27381  lrrecfr  27407  hpgerlem  27996  axcontlem4  28205  axcontlem10  28211  upgrex  28332  fusgrn0degnn0  28736  uhgrvd00  28771  wspthsnonn0vne  29151  eulerpath  29474  frgrwopreglem2  29546  ubthlem1  30101  shintcli  30560  2ndimaxp  31850  fpwrelmapffslem  31935  qsxpid  32443  qsidomlem2  32530  qsdrng  32564  dimcl  32634  lmimdim  32635  lvecdim0i  32636  lvecdim0  32637  lssdimle  32638  dimpropd  32639  dimkerim  32657  fedgmul  32661  extdg1id  32687  fmcncfil  32849  insiga  33073  unelldsys  33094  bnj1189  33958  bnj1279  33967  pconnconn  34160  txsconn  34170  cvmsss2  34203  cvmopnlem  34207  cvmfolem  34208  cvmliftmolem2  34211  cvmlift2lem10  34241  cvmliftpht  34247  cvmlift3lem8  34255  eldm3  34669  fundmpss  34676  elima4  34685  neibastop1  35182  neibastop2lem  35183  neibastop2  35184  fnemeet2  35190  fnejoin2  35192  neifg  35194  tailfb  35200  filnetlem3  35203  bj-n0i  35770  bj-rest10  35907  bj-restn0  35909  poimirlem30  36456  itg2addnclem2  36478  prdsbnd2  36601  heibor1lem  36615  bfp  36630  divrngidl  36834  rnxrn  37206  trcoss2  37292  atex  38215  llnn0  38325  lplnn0N  38356  lvoln0N  38400  pmapglb2N  38580  pmapglb2xN  38581  elpaddn0  38609  osumcllem8N  38772  pexmidlem5N  38783  diaglbN  39864  diaintclN  39867  dibglbN  39975  dibintclN  39976  dihglblem2aN  40102  dihglblem5  40107  dihglbcpreN  40109  dihintcl  40153  ricsym  41043  rictr  41044  riccrng1  41045  ricdrng1  41051  rencldnfilem  41491  kelac1  41738  lnmlmic  41763  gicabl  41774  neik0pk1imk0  42731  ntrneineine0lem  42767  scotteld  42938  onfrALT  43243  onfrALTVD  43585  iunconnlem2  43629  snelmap  43704  eliin2f  43726  disjinfi  43824  mapss2  43837  difmap  43839  infrpge  43996  infxrlesupxr  44081  inficc  44182  fsumnncl  44223  ellimciota  44265  islpcn  44290  lptre2pt  44291  stoweidlem35  44686  fourierdlem31  44789  fourier2  44878  qndenserrnbllem  44945  qndenserrnopn  44949  qndenserrn  44950  intsaluni  44980  sge0cl  45032  ovn0lem  45216  ovnsubaddlem2  45222  hoidmvval0b  45241  hspdifhsp  45267  fsetprcnexALT  45707  uniimaelsetpreimafv  45999  imasetpreimafvbijlemfv1  46006  mgmpropd  46480  opmpoismgm  46512  subrngint  46672  nzerooringczr  46872  neircl  47439  thincn0eu  47554  thinccic  47583  prstchom2ALT  47601  alscn0d  47744