Theorem n0 4316

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

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

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 3917  df-nul 4297

This theorem is referenced by:  reximdva0  4318  rspn0  4319  n0rex  4320  n0moeu  4322  eqeuel  4328  ndisj  4333  pssnel  4434  r19.2z  4458  r19.2zb  4459  r19.3rz  4460  uniintsn  4949  iunn0  5031  trintss  5233  intex  5299  notzfaus  5318  reusv2lem1  5353  nnullss  5422  exss  5423  opabn0  5513  wefrc  5632  wereu2  5635  dmxp  5892  dmxpOLD  5893  xpnz  6132  dmsnn0  6180  unixp0  6256  xpco  6262  frpomin  6313  onfr  6371  iotanul2  6481  fveqdmss  7050  eldmrexrnb  7064  isofrlem  7315  limuni3  7828  soex  7897  f1oweALT  7951  fo1stres  7994  fo2ndres  7995  ecdmn0  8723  fsetprcnex  8835  map0g  8857  ixpn0  8903  resixpfo  8909  domdifsn  9024  xpdom3  9039  fodomr  9092  mapdom3  9113  0sdom1dom  9185  unblem2  9240  fodomfir  9279  marypha1lem  9384  brwdom2  9526  unxpwdom2  9541  ixpiunwdom  9543  zfreg  9548  epfrs  9684  frmin  9702  scott0  9839  cplem1  9842  fseqen  9980  finacn  10003  iunfictbso  10067  aceq2  10072  dfac3  10074  dfac9  10090  kmlem6  10109  kmlem8  10111  infpss  10169  fin23lem7  10269  enfin2i  10274  fin23lem21  10292  fin23lem31  10296  isf32lem9  10314  isf34lem4  10330  axdc2lem  10401  axdc3lem4  10406  ac6c4  10434  ac9  10436  ac6s4  10443  ac9s  10446  ttukeyg  10470  fpwwe2lem11  10594  wun0  10671  tsk0  10716  gruina  10771  genpn0  10956  prlem934  10986  ltaddpr  10987  ltexprlem1  10989  prlem936  11000  reclem2pr  11001  suplem1pr  11005  supsr  11065  axpre-sup  11122  dedekind  11337  dedekindle  11338  negn0  11607  infm3  12142  supaddc  12150  supadd  12151  supmul1  12152  supmullem2  12154  supmul  12155  zsupss  12896  xrsupsslem  13267  xrinfmsslem  13268  supxrre  13287  infxrre  13297  ixxub  13327  ixxlb  13328  ioorebas  13412  fzn0  13499  fzon0  13638  hashgt0elexb  14367  swrdcl  14610  pfxcl  14642  maxprmfct  16679  4sqlem12  16927  vdwmc  16949  ramz  16996  ramub1  16999  mreiincl  17557  mremre  17565  mreexexlem4d  17608  iscatd2  17642  catcone0  17648  cic  17761  drsdirfi  18266  mgmpropd  18578  opifismgm  18586  dfgrp3lem  18970  dfgrp3e  18972  issubg2  19073  subgint  19082  giclcl  19205  gicrcl  19206  gicsym  19207  gictr  19208  gicen  19210  gicsubgen  19211  cntzssv  19260  symggen  19400  psgnunilem3  19426  sylow1lem4  19531  odcau  19534  sylow3  19563  cyggex2  19827  giccyg  19830  pgpfac1lem5  20011  brric2  20415  subrngint  20469  subrgint  20504  abvn0b  20745  lss0cl  20853  lmiclcl  20977  lmicrcl  20978  lmicsym  20979  lspsnat  21055  lspprat  21063  cnsubrg  21344  nzerooringczr  21390  cygzn  21480  lmiclbs  21746  lmisfree  21751  lmictra  21754  mpfrcl  21992  ply1frcl  22205  mdetdiaglem  22485  mdet0  22493  toponmre  22980  iunconnlem  23314  iunconn  23315  unconn  23316  clsconn  23317  2ndcdisj  23343  2ndcsep  23346  1stcelcls  23348  locfincmp  23413  comppfsc  23419  txcls  23491  hmphsym  23669  hmphtr  23670  hmphen  23672  haushmphlem  23674  cmphmph  23675  connhmph  23676  reghmph  23680  nrmhmph  23681  hmphdis  23683  hmphen2  23686  fbdmn0  23721  isfbas2  23722  fbssint  23725  trfbas2  23730  filtop  23742  isfil2  23743  elfg  23758  fgcl  23765  filssufilg  23798  uffix2  23811  ufildom1  23813  hauspwpwf1  23874  hausflf2  23885  alexsubALTlem2  23935  ptcmplem2  23940  cnextf  23953  tgptsmscld  24038  ustfilxp  24100  xbln0  24302  lpbl  24391  met2ndci  24410  metustfbas  24445  restmetu  24458  reconn  24717  opnreen  24720  metdsre  24742  phtpcer  24894  phtpc01  24895  phtpcco2  24899  pcohtpy  24920  cfilfcls  25174  cmetcaulem  25188  cmetcau  25189  bcthlem5  25228  ovolicc2lem2  25419  ovolicc2lem5  25422  ioorcl2  25473  ioorinv2  25476  itg11  25592  dvlip  25898  dvne0  25916  fta1g  26075  plyssc  26105  fta1  26216  vieta1lem2  26219  nocvxmin  27690  sslttr  27719  sltlpss  27819  lrrecfr  27850  onscutlt  28165  hpgerlem  28692  axcontlem4  28894  axcontlem10  28900  upgrex  29019  fusgrn0degnn0  29427  uhgrvd00  29462  wspthsnonn0vne  29847  eulerpath  30170  frgrwopreglem2  30242  ubthlem1  30799  shintcli  31258  n0limd  32401  2ndimaxp  32570  fpwrelmapffslem  32655  qsxpid  33333  qsidomlem2  33424  qsdrng  33468  1arithidom  33508  dimcl  33598  lmimdim  33599  lmicdim  33600  lvecdim0i  33601  lvecdim0  33602  lssdimle  33603  dimpropd  33604  dimkerim  33623  fedgmul  33627  extdg1id  33661  fmcncfil  33921  insiga  34127  unelldsys  34148  bnj1189  34999  bnj1279  35008  pconnconn  35218  txsconn  35228  cvmsss2  35261  cvmopnlem  35265  cvmfolem  35266  cvmliftmolem2  35269  cvmlift2lem10  35299  cvmliftpht  35305  cvmlift3lem8  35313  eldm3  35748  fundmpss  35754  elima4  35763  neibastop1  36347  neibastop2lem  36348  neibastop2  36349  fnemeet2  36355  fnejoin2  36357  neifg  36359  tailfb  36365  filnetlem3  36368  bj-n0i  36939  bj-rest10  37076  bj-restn0  37078  poimirlem30  37644  itg2addnclem2  37666  prdsbnd2  37789  heibor1lem  37803  bfp  37818  divrngidl  38022  eldmres3  38265  rnxrn  38384  eldmxrncnvepres2  38397  trcoss2  38475  atex  39400  llnn0  39510  lplnn0N  39541  lvoln0N  39585  pmapglb2N  39765  pmapglb2xN  39766  elpaddn0  39794  osumcllem8N  39957  pexmidlem5N  39968  diaglbN  41049  diaintclN  41052  dibglbN  41160  dibintclN  41161  dihglblem2aN  41287  dihglblem5  41292  dihglbcpreN  41294  dihintcl  41338  unitscyglem5  42187  ricsym  42507  rictr  42508  riccrng1  42509  ricdrng1  42516  rencldnfilem  42808  kelac1  43052  lnmlmic  43077  gicabl  43088  neik0pk1imk0  44036  ntrneineine0lem  44072  scotteld  44235  onfrALT  44539  onfrALTVD  44880  iunconnlem2  44924  relpfrlem  44943  dfac5prim  44980  permac8prim  45004  snelmap  45076  eliin2f  45098  disjinfi  45186  mapss2  45199  difmap  45201  infrpge  45347  infxrlesupxr  45432  inficc  45532  fsumnncl  45570  ellimciota  45612  islpcn  45637  lptre2pt  45638  stoweidlem35  46033  fourierdlem31  46136  fourier2  46225  qndenserrnbllem  46292  qndenserrnopn  46296  qndenserrn  46297  intsaluni  46327  sge0cl  46379  ovn0lem  46563  ovnsubaddlem2  46569  hoidmvval0b  46588  hspdifhsp  46614  fsetprcnexALT  47063  uniimaelsetpreimafv  47397  imasetpreimafvbijlemfv1  47404  dfgric2  47915  gricuspgr  47918  gricsym  47921  grictr  47923  gricen  47925  dfgrlic2  48000  dfgrlic3  48002  grlicen  48009  gricgrlic  48010  usgrexmpl12ngric  48029  usgrexmpl12ngrlic  48030  opmpoismgm  48155  neircl  48893  sectrcl  49011  invrcl  49013  isorcl  49022  iinfssc  49046  iinfsubc  49047  imaid  49143  thincn0eu  49420  thinccic  49460  termcterm2  49503  eufunc  49511  euendfunc  49515  diag1f1o  49523  diag2f1o  49526  prstchom2ALT  49553  rellan  49612  relran  49613  alscn0d  49784