Theorem n0 4376

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1537  ∃wex 1777   ∈ wcel 2108   ≠ wne 2946  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-ne 2947  df-dif 3979  df-nul 4353

This theorem is referenced by:  reximdva0  4378  rspn0  4379  n0rex  4380  n0moeu  4382  eqeuel  4388  ndisj  4393  pssnel  4494  r19.2z  4518  r19.2zb  4519  r19.3rz  4520  uniintsn  5009  iunn0  5090  trintss  5302  intex  5362  notzfaus  5381  reusv2lem1  5416  nnullss  5482  exss  5483  opabn0  5572  wefrc  5694  wereu2  5697  dmxp  5953  dmxpOLD  5954  xpnz  6190  dmsnn0  6238  unixp0  6314  xpco  6320  frpomin  6372  onfr  6434  iotanul2  6543  fveqdmss  7112  eldmrexrnb  7126  isofrlem  7376  limuni3  7889  soex  7961  f1oweALT  8013  fo1stres  8056  fo2ndres  8057  ecdmn0  8812  fsetprcnex  8920  map0g  8942  ixpn0  8988  resixpfo  8994  domdifsn  9120  xpdom3  9136  fodomr  9194  mapdom3  9215  0sdom1dom  9301  unblem2  9357  fodomfir  9396  marypha1lem  9502  brwdom2  9642  unxpwdom2  9657  ixpiunwdom  9659  zfreg  9664  epfrs  9800  frmin  9818  scott0  9955  cplem1  9958  fseqen  10096  finacn  10119  iunfictbso  10183  aceq2  10188  dfac3  10190  dfac9  10206  kmlem6  10225  kmlem8  10227  infpss  10285  fin23lem7  10385  enfin2i  10390  fin23lem21  10408  fin23lem31  10412  isf32lem9  10430  isf34lem4  10446  axdc2lem  10517  axdc3lem4  10522  ac6c4  10550  ac9  10552  ac6s4  10559  ac9s  10562  ttukeyg  10586  fpwwe2lem11  10710  wun0  10787  tsk0  10832  gruina  10887  genpn0  11072  prlem934  11102  ltaddpr  11103  ltexprlem1  11105  prlem936  11116  reclem2pr  11117  suplem1pr  11121  supsr  11181  axpre-sup  11238  dedekind  11453  dedekindle  11454  negn0  11719  infm3  12254  supaddc  12262  supadd  12263  supmul1  12264  supmullem2  12266  supmul  12267  zsupss  13002  xrsupsslem  13369  xrinfmsslem  13370  supxrre  13389  infxrre  13398  ixxub  13428  ixxlb  13429  ioorebas  13511  fzn0  13598  fzon0  13734  hashgt0elexb  14451  swrdcl  14693  pfxcl  14725  maxprmfct  16756  4sqlem12  17003  vdwmc  17025  ramz  17072  ramub1  17075  mreiincl  17654  mremre  17662  mreexexlem4d  17705  iscatd2  17739  catcone0  17745  cic  17860  drsdirfi  18375  mgmpropd  18689  opifismgm  18697  dfgrp3lem  19078  dfgrp3e  19080  issubg2  19181  subgint  19190  giclcl  19313  gicrcl  19314  gicsym  19315  gictr  19316  gicen  19318  gicsubgen  19319  cntzssv  19368  symggen  19512  psgnunilem3  19538  sylow1lem4  19643  odcau  19646  sylow3  19675  cyggex2  19939  giccyg  19942  pgpfac1lem5  20123  brric2  20532  subrngint  20586  subrgint  20623  abvn0b  20859  lss0cl  20968  lmiclcl  21092  lmicrcl  21093  lmicsym  21094  lspsnat  21170  lspprat  21178  cnsubrg  21468  nzerooringczr  21514  cygzn  21612  lmiclbs  21880  lmisfree  21885  lmictra  21888  mpfrcl  22132  ply1frcl  22343  mdetdiaglem  22625  mdet0  22633  toponmre  23122  iunconnlem  23456  iunconn  23457  unconn  23458  clsconn  23459  2ndcdisj  23485  2ndcsep  23488  1stcelcls  23490  locfincmp  23555  comppfsc  23561  txcls  23633  hmphsym  23811  hmphtr  23812  hmphen  23814  haushmphlem  23816  cmphmph  23817  connhmph  23818  reghmph  23822  nrmhmph  23823  hmphdis  23825  hmphen2  23828  fbdmn0  23863  isfbas2  23864  fbssint  23867  trfbas2  23872  filtop  23884  isfil2  23885  elfg  23900  fgcl  23907  filssufilg  23940  uffix2  23953  ufildom1  23955  hauspwpwf1  24016  hausflf2  24027  alexsubALTlem2  24077  ptcmplem2  24082  cnextf  24095  tgptsmscld  24180  ustfilxp  24242  xbln0  24445  lpbl  24537  met2ndci  24556  metustfbas  24591  restmetu  24604  reconn  24869  opnreen  24872  metdsre  24894  phtpcer  25046  phtpc01  25047  phtpcco2  25051  pcohtpy  25072  cfilfcls  25327  cmetcaulem  25341  cmetcau  25342  bcthlem5  25381  ovolicc2lem2  25572  ovolicc2lem5  25575  ioorcl2  25626  ioorinv2  25629  itg11  25745  dvlip  26052  dvne0  26070  fta1g  26229  plyssc  26259  fta1  26368  vieta1lem2  26371  nocvxmin  27841  sslttr  27870  sltlpss  27963  lrrecfr  27994  hpgerlem  28791  axcontlem4  29000  axcontlem10  29006  upgrex  29127  fusgrn0degnn0  29535  uhgrvd00  29570  wspthsnonn0vne  29950  eulerpath  30273  frgrwopreglem2  30345  ubthlem1  30902  shintcli  31361  n0limd  32501  2ndimaxp  32665  fpwrelmapffslem  32746  qsxpid  33355  qsidomlem2  33446  qsdrng  33490  1arithidom  33530  dimcl  33615  lmimdim  33616  lmicdim  33617  lvecdim0i  33618  lvecdim0  33619  lssdimle  33620  dimpropd  33621  dimkerim  33640  fedgmul  33644  extdg1id  33676  fmcncfil  33877  insiga  34101  unelldsys  34122  bnj1189  34985  bnj1279  34994  pconnconn  35199  txsconn  35209  cvmsss2  35242  cvmopnlem  35246  cvmfolem  35247  cvmliftmolem2  35250  cvmlift2lem10  35280  cvmliftpht  35286  cvmlift3lem8  35294  eldm3  35723  fundmpss  35730  elima4  35739  neibastop1  36325  neibastop2lem  36326  neibastop2  36327  fnemeet2  36333  fnejoin2  36335  neifg  36337  tailfb  36343  filnetlem3  36346  bj-n0i  36917  bj-rest10  37054  bj-restn0  37056  poimirlem30  37610  itg2addnclem2  37632  prdsbnd2  37755  heibor1lem  37769  bfp  37784  divrngidl  37988  rnxrn  38354  trcoss2  38440  atex  39363  llnn0  39473  lplnn0N  39504  lvoln0N  39548  pmapglb2N  39728  pmapglb2xN  39729  elpaddn0  39757  osumcllem8N  39920  pexmidlem5N  39931  diaglbN  41012  diaintclN  41015  dibglbN  41123  dibintclN  41124  dihglblem2aN  41250  dihglblem5  41255  dihglbcpreN  41257  dihintcl  41301  unitscyglem5  42156  ricsym  42474  rictr  42475  riccrng1  42476  ricdrng1  42483  rencldnfilem  42776  kelac1  43020  lnmlmic  43045  gicabl  43056  neik0pk1imk0  44009  ntrneineine0lem  44045  scotteld  44215  onfrALT  44520  onfrALTVD  44862  iunconnlem2  44906  snelmap  44984  eliin2f  45006  disjinfi  45099  mapss2  45112  difmap  45114  infrpge  45266  infxrlesupxr  45351  inficc  45452  fsumnncl  45493  ellimciota  45535  islpcn  45560  lptre2pt  45561  stoweidlem35  45956  fourierdlem31  46059  fourier2  46148  qndenserrnbllem  46215  qndenserrnopn  46219  qndenserrn  46220  intsaluni  46250  sge0cl  46302  ovn0lem  46486  ovnsubaddlem2  46492  hoidmvval0b  46511  hspdifhsp  46537  fsetprcnexALT  46977  uniimaelsetpreimafv  47270  imasetpreimafvbijlemfv1  47277  dfgric2  47768  gricuspgr  47771  gricsym  47774  grictr  47776  gricen  47778  dfgrlic2  47825  dfgrlic3  47827  grlicen  47834  gricgrlic  47835  usgrexmpl12ngric  47853  usgrexmpl12ngrlic  47854  opmpoismgm  47890  neircl  48584  thincn0eu  48699  thinccic  48728  prstchom2ALT  48746  alscn0d  48889