Theorem n0 4300

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2956  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-ne 2957  df-dif 3902  df-nul 4280

This theorem is used by:  n0limd  4301  reximdva0  4303  rspn0  4304  n0rex  4305  n0moeu  4307  eqeuel  4313  ndisj  4318  pssnel  4424  r19.2z  4455  r19.3rz  4457  uniintsn  4945  iunn0  5025  trintss  5231  intex  5305  notsep  5325  reusv2lem1  5360  nnullss  5430  exss  5431  opabn0  5528  wefrc  5645  wereu2  5648  dmxp  5911  xpnz  6149  dmsnn0  6201  unixp0  6279  xpco  6285  frpomin  6336  onfr  6395  iotanul2  6504  fveqdmss  7070  eldmrexrnb  7084  isofrlem  7340  limuni3  7852  soex  7922  f1oweALT  7973  fo1stres  8016  fo2ndres  8017  ecdmn0  8754  fsetprcnex  8868  map0g  8896  ixpn0  8942  resixpfo  8948  domdifsn  9063  xpdom3  9078  fodomr  9131  mapdom3  9152  0sdom1dom  9221  unblem2  9269  fodomfir  9303  marypha1lem  9409  brwdom2  9551  unxpwdom2  9566  ixpiunwdom  9568  zfreg  9574  epfrs  9716  frmin  9737  scott0b  9918  scott0OLD  9919  scotteld  9928  cplem1  9931  cplem1OLD  9932  karden  9940  fseqen  10087  finacn  10110  iunfictbso  10174  aceq2  10179  dfac3  10181  dfac9  10196  kmlem6  10215  kmlem8  10217  infpss  10275  fin23lem7  10375  enfin2i  10380  fin23lem21  10398  fin23lem31  10402  isf32lem9  10420  isf34lem4  10436  axdc2lem  10507  axdc3lem4  10512  ac6c4  10540  ac9  10542  ac6s4  10549  ac9s  10552  ttukeyg  10576  fpwwe2lem11  10707  wun0  10784  tsk0  10829  gruina  10884  genpn0  11069  prlem934  11099  ltaddpr  11100  ltexprlem1  11102  prlem936  11113  reclem2pr  11114  suplem1pr  11118  supsr  11178  axpre-sup  11235  dedekind  11454  dedekindle  11455  negn0  11726  infm3  12257  supaddc  12265  supadd  12266  supmul1  12267  supmullem2  12269  supmul  12270  zsupss  13045  xrsupsslem  13418  xrinfmsslem  13419  supxrre  13438  infxrre  13448  ixxub  13478  ixxlb  13479  ioorebas  13563  fzn0  13651  fzon0  13792  hashgt0elexb  14526  swrdcl  14773  pfxcl  14807  maxprmfct  16865  4sqlem12  17114  vdwmc  17136  ramz  17183  ramub1  17186  mreiincl  17746  mremre  17754  mreexexlem4d  17801  iscatd2  17835  catcone0  17841  cic  17954  drsdirfi  18459  mgmpropd  18809  opifismgm  18817  dfgrp3lem  19228  dfgrp3e  19230  issubg2  19332  subgint  19341  qsxpid  19367  giclcl  19467  gicrcl  19468  gicsym  19469  gictr  19470  gicen  19472  gicsubgen  19473  cntzssv  19522  symggen  19664  psgnunilem3  19690  sylow1lem4  19795  odcau  19798  sylow3  19827  cyggex2  20091  giccyg  20094  pgpfac1lem5  20275  riclcl  20729  ricrcl  20730  ricsym  20731  rictr  20732  isbrric2  20733  subrngint  20792  subrgint  20827  abvn0b  21073  lss0cl  21202  lmiclcl  21325  lmicrcl  21326  lmicsym  21327  lspsnat  21403  lspprat  21411  lidlunin0  21495  qsidomlem2  21617  cnsubrg  21713  nzerooringczr  21766  cygzn  21856  lmiclbs  22123  lmisfree  22128  lmictra  22131  mpfrcl  22374  ply1frcl  22616  mdetdiaglem  22893  mdet0  22901  toponmre  23391  iunconnlem  23725  iunconn  23726  unconn  23727  clsconn  23728  2ndcdisj  23755  2ndcsep  23758  1stcelcls  23760  locfincmp  23825  comppfsc  23831  txcls  23903  hmphsym  24081  hmphtr  24082  hmphen  24084  haushmphlem  24086  cmphmph  24087  connhmph  24088  reghmph  24092  nrmhmph  24093  hmphdis  24095  hmphen2  24098  fbdmn0  24133  isfbas2  24134  fbssint  24137  trfbas2  24142  filtop  24154  isfil2  24155  elfg  24170  fgcl  24177  filssufilg  24210  uffix2  24223  ufildom1  24225  hauspwpwf1  24286  hausflf2  24297  alexsubALTlem2  24347  ptcmplem2  24352  cnextf  24365  tgptsmscld  24450  ustfilxp  24512  xbln0  24713  lpbl  24802  met2ndci  24821  metustfbas  24856  restmetu  24869  reconn  25128  opnreen  25131  metdsre  25153  phtpcer  25296  phtpc01  25297  phtpcco2  25300  pcohtpy  25321  cfilfcls  25575  cmetcaulem  25589  cmetcau  25590  bcthlem5  25629  ovolicc2lem2  25819  ovolicc2lem5  25822  ioorcl2  25873  ioorinv2  25876  itg11  25992  dvlip  26293  dvne0  26311  fta1g  26468  plyssc  26498  fta1  26611  vieta1lem2  26616  nobdaymin  28121  sltstr  28155  ltslpss  28276  lrrecfr  28311  oncutlt  28632  hpgerlem  29225  axcontlem4  29527  axcontlem10  29533  upgrex  29652  fusgrn0degnn0  30062  uhgrvd00  30097  wspthsnonn0vne  30488  eulerpath  30824  frgrwopreglem2  30896  ubthlem1  31454  shintcli  31913  2ndimaxp  33222  fpwrelmapffslem  33306  qsdrng  34003  1arithidom  34051  dimcl  34217  lmimdim  34218  lmicdim  34219  lvecdim0i  34220  lvecdim0  34221  lssdimle  34222  dimpropd  34223  dimkerim  34241  fedgmul  34245  extdg1id  34280  fmcncfil  34545  insiga  34752  unelldsys  34773  bnj1189  35622  bnj1279  35631  rankscott  35730  axregszf  35770  karddom  35802  kardsdom  35803  vonf1oonfo  35867  pconnconn  35965  txsconn  35975  cvmsss2  36008  cvmopnlem  36012  cvmfolem  36013  cvmliftmolem2  36016  cvmlift2lem10  36046  cvmliftpht  36052  cvmlift3lem8  36060  eldm3  36495  fundmpss  36501  elima4  36510  neibastop1  37117  neibastop2lem  37118  neibastop2  37119  fnemeet2  37125  fnejoin2  37127  neifg  37129  tailfb  37135  filnetlem3  37138  mh-infprim1bi  37304  bj-n0i  37834  bj-rest10  37977  bj-restn0  37979  poimirlem30  38536  itg2addnclem2  38558  prdsbnd2  38697  heibor1lem  38711  bfp  38726  divrngidl  38930  eldmres3  39183  rnxrn  39321  eldmxrncnvepres2  39335  trcoss2  39474  atex  40431  llnn0  40541  lplnn0N  40572  lvoln0N  40616  pmapglb2N  40796  pmapglb2xN  40797  elpaddn0  40825  osumcllem8N  40988  pexmidlem5N  40999  diaglbN  42080  diaintclN  42083  dibglbN  42191  dibintclN  42192  dihglblem2aN  42318  dihglblem5  42323  dihglbcpreN  42325  dihintcl  42369  unitscyglem5  43217  riccrng1  43547  ricdrng1  43554  rencldnfilem  43780  kelac1  44023  lnmlmic  44048  gicabl  44059  neik0pk1imk0  45006  ntrneineine0lem  45042  onfrALT  45491  onfrALTVD  45832  iunconnlem2  45876  relpfrlem  45895  dfac5prim  45932  permac8prim  45956  snelmap  46042  eliin2f  46062  disjinfi  46150  mapss2  46162  difmap  46163  infrpge  46307  infxrlesupxr  46390  inficc  46490  fsumnncl  46528  ellimciota  46570  islpcn  46593  lptre2pt  46594  stoweidlem35  46989  fourierdlem31  47092  fourier2  47181  qndenserrnbllem  47248  qndenserrnopn  47252  qndenserrn  47253  intsaluni  47283  sge0cl  47335  ovn0lem  47519  ovnsubaddlem2  47525  hoidmvval0b  47544  hspdifhsp  47570  fsetprcnexALT  48076  uniimaelsetpreimafv  48422  imasetpreimafvbijlemfv1  48429  dfgric2  48957  gricuspgr  48960  gricsym  48963  grictr  48965  gricen  48967  dfgrlic2  49050  dfgrlic3  49052  grlicen  49059  gricgrlic  49060  usgrexmpl12ngric  49080  usgrexmpl12ngrlic  49081  opmpoismgm  49208  neircl  49957  sectrcl  50074  invrcl  50076  isorcl  50085  iinfssc  50109  iinfsubc  50110  imaid  50206  thincn0eu  50483  thinccic  50523  termcterm2  50566  eufunc  50574  euendfunc  50578  diag1f1o  50586  diag2f1o  50589  prstchom2ALT  50616  rellan  50675  relran  50676  alsralrex  50852