Theorem n0 4294

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 2163, ax-12 2185. (Revised by GG, 28-Jun-2024.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2933  ∅c0 4274

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ne 2934  df-dif 3893  df-nul 4275

This theorem is referenced by:  reximdva0  4296  rspn0  4297  n0rex  4298  n0moeu  4300  eqeuel  4306  ndisj  4311  pssnel  4412  r19.2z  4440  r19.3rz  4442  uniintsn  4928  iunn0  5010  trintss  5211  intex  5279  notzfaus  5298  reusv2lem1  5333  nnullss  5407  exss  5408  opabn0  5499  wefrc  5616  wereu2  5619  dmxp  5876  xpnz  6115  dmsnn0  6163  unixp0  6239  xpco  6245  frpomin  6296  onfr  6354  iotanul2  6463  fveqdmss  7022  eldmrexrnb  7036  isofrlem  7286  limuni3  7794  soex  7863  f1oweALT  7916  fo1stres  7959  fo2ndres  7960  ecdmn0  8687  fsetprcnex  8800  map0g  8823  ixpn0  8869  resixpfo  8875  domdifsn  8989  xpdom3  9004  fodomr  9057  mapdom3  9078  0sdom1dom  9147  unblem2  9194  fodomfir  9229  marypha1lem  9337  brwdom2  9479  unxpwdom2  9494  ixpiunwdom  9496  zfreg  9502  epfrs  9641  frmin  9662  scott0  9799  cplem1  9802  fseqen  9938  finacn  9961  iunfictbso  10025  aceq2  10030  dfac3  10032  dfac9  10048  kmlem6  10067  kmlem8  10069  infpss  10127  fin23lem7  10227  enfin2i  10232  fin23lem21  10250  fin23lem31  10254  isf32lem9  10272  isf34lem4  10288  axdc2lem  10359  axdc3lem4  10364  ac6c4  10392  ac9  10394  ac6s4  10401  ac9s  10404  ttukeyg  10428  fpwwe2lem11  10553  wun0  10630  tsk0  10675  gruina  10730  genpn0  10915  prlem934  10945  ltaddpr  10946  ltexprlem1  10948  prlem936  10959  reclem2pr  10960  suplem1pr  10964  supsr  11024  axpre-sup  11081  dedekind  11298  dedekindle  11299  negn0  11568  infm3  12104  supaddc  12112  supadd  12113  supmul1  12114  supmullem2  12116  supmul  12117  zsupss  12876  xrsupsslem  13248  xrinfmsslem  13249  supxrre  13268  infxrre  13278  ixxub  13308  ixxlb  13309  ioorebas  13393  fzn0  13481  fzon0  13621  hashgt0elexb  14353  swrdcl  14597  pfxcl  14629  maxprmfct  16668  4sqlem12  16916  vdwmc  16938  ramz  16985  ramub1  16988  mreiincl  17547  mremre  17555  mreexexlem4d  17602  iscatd2  17636  catcone0  17642  cic  17755  drsdirfi  18260  mgmpropd  18608  opifismgm  18616  dfgrp3lem  19003  dfgrp3e  19005  issubg2  19106  subgint  19115  giclcl  19237  gicrcl  19238  gicsym  19239  gictr  19240  gicen  19242  gicsubgen  19243  cntzssv  19292  symggen  19434  psgnunilem3  19460  sylow1lem4  19565  odcau  19568  sylow3  19597  cyggex2  19861  giccyg  19864  pgpfac1lem5  20045  brric2  20472  subrngint  20526  subrgint  20561  abvn0b  20802  lss0cl  20931  lmiclcl  21055  lmicrcl  21056  lmicsym  21057  lspsnat  21133  lspprat  21141  cnsubrg  21415  nzerooringczr  21468  cygzn  21558  lmiclbs  21825  lmisfree  21830  lmictra  21833  mpfrcl  22072  ply1frcl  22292  mdetdiaglem  22572  mdet0  22580  toponmre  23067  iunconnlem  23401  iunconn  23402  unconn  23403  clsconn  23404  2ndcdisj  23430  2ndcsep  23433  1stcelcls  23435  locfincmp  23500  comppfsc  23506  txcls  23578  hmphsym  23756  hmphtr  23757  hmphen  23759  haushmphlem  23761  cmphmph  23762  connhmph  23763  reghmph  23767  nrmhmph  23768  hmphdis  23770  hmphen2  23773  fbdmn0  23808  isfbas2  23809  fbssint  23812  trfbas2  23817  filtop  23829  isfil2  23830  elfg  23845  fgcl  23852  filssufilg  23885  uffix2  23898  ufildom1  23900  hauspwpwf1  23961  hausflf2  23972  alexsubALTlem2  24022  ptcmplem2  24027  cnextf  24040  tgptsmscld  24125  ustfilxp  24187  xbln0  24388  lpbl  24477  met2ndci  24496  metustfbas  24531  restmetu  24544  reconn  24803  opnreen  24806  metdsre  24828  phtpcer  24971  phtpc01  24972  phtpcco2  24975  pcohtpy  24996  cfilfcls  25250  cmetcaulem  25264  cmetcau  25265  bcthlem5  25304  ovolicc2lem2  25494  ovolicc2lem5  25497  ioorcl2  25548  ioorinv2  25551  itg11  25667  dvlip  25970  dvne0  25988  fta1g  26147  plyssc  26177  fta1  26287  vieta1lem2  26290  nobdaymin  27764  sltstr  27798  ltslpss  27919  lrrecfr  27954  oncutlt  28275  hpgerlem  28852  axcontlem4  29055  axcontlem10  29061  upgrex  29180  fusgrn0degnn0  29588  uhgrvd00  29623  wspthsnonn0vne  30005  eulerpath  30331  frgrwopreglem2  30403  ubthlem1  30961  shintcli  31420  n0limd  32561  2ndimaxp  32739  fpwrelmapffslem  32825  qsxpid  33442  qsidomlem2  33533  qsdrng  33577  1arithidom  33617  dimcl  33767  lmimdim  33768  lmicdim  33769  lvecdim0i  33770  lvecdim0  33771  lssdimle  33772  dimpropd  33773  dimkerim  33792  fedgmul  33796  extdg1id  33831  fmcncfil  34096  insiga  34302  unelldsys  34323  bnj1189  35172  bnj1279  35181  axregszf  35294  pconnconn  35434  txsconn  35444  cvmsss2  35477  cvmopnlem  35481  cvmfolem  35482  cvmliftmolem2  35485  cvmlift2lem10  35515  cvmliftpht  35521  cvmlift3lem8  35529  eldm3  35964  fundmpss  35970  elima4  35979  neibastop1  36562  neibastop2lem  36563  neibastop2  36564  fnemeet2  36570  fnejoin2  36572  neifg  36574  tailfb  36580  filnetlem3  36583  bj-n0i  37271  bj-rest10  37413  bj-restn0  37415  poimirlem30  37982  itg2addnclem2  38004  prdsbnd2  38127  heibor1lem  38141  bfp  38156  divrngidl  38360  eldmres3  38615  rnxrn  38753  eldmxrncnvepres2  38767  trcoss2  38906  atex  39863  llnn0  39973  lplnn0N  40004  lvoln0N  40048  pmapglb2N  40228  pmapglb2xN  40229  elpaddn0  40257  osumcllem8N  40420  pexmidlem5N  40431  diaglbN  41512  diaintclN  41515  dibglbN  41623  dibintclN  41624  dihglblem2aN  41750  dihglblem5  41755  dihglbcpreN  41757  dihintcl  41801  unitscyglem5  42649  ricsym  42975  rictr  42976  riccrng1  42977  ricdrng1  42984  rencldnfilem  43263  kelac1  43506  lnmlmic  43531  gicabl  43542  neik0pk1imk0  44489  ntrneineine0lem  44525  scotteld  44688  onfrALT  44991  onfrALTVD  45332  iunconnlem2  45376  relpfrlem  45395  dfac5prim  45432  permac8prim  45456  snelmap  45528  eliin2f  45549  disjinfi  45637  mapss2  45649  difmap  45651  infrpge  45796  infxrlesupxr  45879  inficc  45979  fsumnncl  46017  ellimciota  46059  islpcn  46082  lptre2pt  46083  stoweidlem35  46478  fourierdlem31  46581  fourier2  46670  qndenserrnbllem  46737  qndenserrnopn  46741  qndenserrn  46742  intsaluni  46772  sge0cl  46824  ovn0lem  47008  ovnsubaddlem2  47014  hoidmvval0b  47033  hspdifhsp  47059  fsetprcnexALT  47507  uniimaelsetpreimafv  47853  imasetpreimafvbijlemfv1  47860  dfgric2  48388  gricuspgr  48391  gricsym  48394  grictr  48396  gricen  48398  dfgrlic2  48481  dfgrlic3  48483  grlicen  48490  gricgrlic  48491  usgrexmpl12ngric  48511  usgrexmpl12ngrlic  48512  opmpoismgm  48640  neircl  49377  sectrcl  49494  invrcl  49496  isorcl  49505  iinfssc  49529  iinfsubc  49530  imaid  49626  thincn0eu  49903  thinccic  49943  termcterm2  49986  eufunc  49994  euendfunc  49998  diag1f1o  50006  diag2f1o  50009  prstchom2ALT  50036  rellan  50095  relran  50096  alscn0d  50267