Theorem n0 4303

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1541  ∃wex 1780   ∈ wcel 2111   ≠ wne 2928  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-ne 2929  df-dif 3905  df-nul 4284

This theorem is referenced by:  reximdva0  4305  rspn0  4306  n0rex  4307  n0moeu  4309  eqeuel  4315  ndisj  4320  pssnel  4421  r19.2z  4445  r19.2zb  4446  r19.3rz  4447  uniintsn  4935  iunn0  5015  trintss  5216  intex  5282  notzfaus  5301  reusv2lem1  5336  nnullss  5402  exss  5403  opabn0  5493  wefrc  5610  wereu2  5613  dmxp  5869  xpnz  6106  dmsnn0  6154  unixp0  6230  xpco  6236  frpomin  6287  onfr  6345  iotanul2  6454  fveqdmss  7011  eldmrexrnb  7025  isofrlem  7274  limuni3  7782  soex  7851  f1oweALT  7904  fo1stres  7947  fo2ndres  7948  ecdmn0  8674  fsetprcnex  8786  map0g  8808  ixpn0  8854  resixpfo  8860  domdifsn  8973  xpdom3  8988  fodomr  9041  mapdom3  9062  0sdom1dom  9130  unblem2  9177  fodomfir  9212  marypha1lem  9317  brwdom2  9459  unxpwdom2  9474  ixpiunwdom  9476  zfreg  9482  epfrs  9621  frmin  9639  scott0  9776  cplem1  9779  fseqen  9915  finacn  9938  iunfictbso  10002  aceq2  10007  dfac3  10009  dfac9  10025  kmlem6  10044  kmlem8  10046  infpss  10104  fin23lem7  10204  enfin2i  10209  fin23lem21  10227  fin23lem31  10231  isf32lem9  10249  isf34lem4  10265  axdc2lem  10336  axdc3lem4  10341  ac6c4  10369  ac9  10371  ac6s4  10378  ac9s  10381  ttukeyg  10405  fpwwe2lem11  10529  wun0  10606  tsk0  10651  gruina  10706  genpn0  10891  prlem934  10921  ltaddpr  10922  ltexprlem1  10924  prlem936  10935  reclem2pr  10936  suplem1pr  10940  supsr  11000  axpre-sup  11057  dedekind  11273  dedekindle  11274  negn0  11543  infm3  12078  supaddc  12086  supadd  12087  supmul1  12088  supmullem2  12090  supmul  12091  zsupss  12832  xrsupsslem  13203  xrinfmsslem  13204  supxrre  13223  infxrre  13233  ixxub  13263  ixxlb  13264  ioorebas  13348  fzn0  13435  fzon0  13574  hashgt0elexb  14306  swrdcl  14550  pfxcl  14582  maxprmfct  16617  4sqlem12  16865  vdwmc  16887  ramz  16934  ramub1  16937  mreiincl  17495  mremre  17503  mreexexlem4d  17550  iscatd2  17584  catcone0  17590  cic  17703  drsdirfi  18208  mgmpropd  18556  opifismgm  18564  dfgrp3lem  18948  dfgrp3e  18950  issubg2  19051  subgint  19060  giclcl  19183  gicrcl  19184  gicsym  19185  gictr  19186  gicen  19188  gicsubgen  19189  cntzssv  19238  symggen  19380  psgnunilem3  19406  sylow1lem4  19511  odcau  19514  sylow3  19543  cyggex2  19807  giccyg  19810  pgpfac1lem5  19991  brric2  20419  subrngint  20473  subrgint  20508  abvn0b  20749  lss0cl  20878  lmiclcl  21002  lmicrcl  21003  lmicsym  21004  lspsnat  21080  lspprat  21088  cnsubrg  21362  nzerooringczr  21415  cygzn  21505  lmiclbs  21772  lmisfree  21777  lmictra  21780  mpfrcl  22018  ply1frcl  22231  mdetdiaglem  22511  mdet0  22519  toponmre  23006  iunconnlem  23340  iunconn  23341  unconn  23342  clsconn  23343  2ndcdisj  23369  2ndcsep  23372  1stcelcls  23374  locfincmp  23439  comppfsc  23445  txcls  23517  hmphsym  23695  hmphtr  23696  hmphen  23698  haushmphlem  23700  cmphmph  23701  connhmph  23702  reghmph  23706  nrmhmph  23707  hmphdis  23709  hmphen2  23712  fbdmn0  23747  isfbas2  23748  fbssint  23751  trfbas2  23756  filtop  23768  isfil2  23769  elfg  23784  fgcl  23791  filssufilg  23824  uffix2  23837  ufildom1  23839  hauspwpwf1  23900  hausflf2  23911  alexsubALTlem2  23961  ptcmplem2  23966  cnextf  23979  tgptsmscld  24064  ustfilxp  24126  xbln0  24327  lpbl  24416  met2ndci  24435  metustfbas  24470  restmetu  24483  reconn  24742  opnreen  24745  metdsre  24767  phtpcer  24919  phtpc01  24920  phtpcco2  24924  pcohtpy  24945  cfilfcls  25199  cmetcaulem  25213  cmetcau  25214  bcthlem5  25253  ovolicc2lem2  25444  ovolicc2lem5  25447  ioorcl2  25498  ioorinv2  25501  itg11  25617  dvlip  25923  dvne0  25941  fta1g  26100  plyssc  26130  fta1  26241  vieta1lem2  26244  nobdaymin  27714  sslttr  27746  sltlpss  27851  lrrecfr  27884  onscutlt  28199  hpgerlem  28741  axcontlem4  28943  axcontlem10  28949  upgrex  29068  fusgrn0degnn0  29476  uhgrvd00  29511  wspthsnonn0vne  29893  eulerpath  30216  frgrwopreglem2  30288  ubthlem1  30845  shintcli  31304  n0limd  32446  2ndimaxp  32623  fpwrelmapffslem  32710  qsxpid  33322  qsidomlem2  33413  qsdrng  33457  1arithidom  33497  dimcl  33610  lmimdim  33611  lmicdim  33612  lvecdim0i  33613  lvecdim0  33614  lssdimle  33615  dimpropd  33616  dimkerim  33635  fedgmul  33639  extdg1id  33674  fmcncfil  33939  insiga  34145  unelldsys  34166  bnj1189  35016  bnj1279  35025  axregszf  35115  pconnconn  35263  txsconn  35273  cvmsss2  35306  cvmopnlem  35310  cvmfolem  35311  cvmliftmolem2  35314  cvmlift2lem10  35344  cvmliftpht  35350  cvmlift3lem8  35358  eldm3  35793  fundmpss  35799  elima4  35808  neibastop1  36392  neibastop2lem  36393  neibastop2  36394  fnemeet2  36400  fnejoin2  36402  neifg  36404  tailfb  36410  filnetlem3  36413  bj-n0i  36984  bj-rest10  37121  bj-restn0  37123  poimirlem30  37689  itg2addnclem2  37711  prdsbnd2  37834  heibor1lem  37848  bfp  37863  divrngidl  38067  eldmres3  38310  rnxrn  38429  eldmxrncnvepres2  38442  trcoss2  38520  atex  39444  llnn0  39554  lplnn0N  39585  lvoln0N  39629  pmapglb2N  39809  pmapglb2xN  39810  elpaddn0  39838  osumcllem8N  40001  pexmidlem5N  40012  diaglbN  41093  diaintclN  41096  dibglbN  41204  dibintclN  41205  dihglblem2aN  41331  dihglblem5  41336  dihglbcpreN  41338  dihintcl  41382  unitscyglem5  42231  ricsym  42551  rictr  42552  riccrng1  42553  ricdrng1  42560  rencldnfilem  42852  kelac1  43095  lnmlmic  43120  gicabl  43131  neik0pk1imk0  44079  ntrneineine0lem  44115  scotteld  44278  onfrALT  44581  onfrALTVD  44922  iunconnlem2  44966  relpfrlem  44985  dfac5prim  45022  permac8prim  45046  snelmap  45118  eliin2f  45140  disjinfi  45228  mapss2  45241  difmap  45243  infrpge  45389  infxrlesupxr  45473  inficc  45573  fsumnncl  45611  ellimciota  45653  islpcn  45676  lptre2pt  45677  stoweidlem35  46072  fourierdlem31  46175  fourier2  46264  qndenserrnbllem  46331  qndenserrnopn  46335  qndenserrn  46336  intsaluni  46366  sge0cl  46418  ovn0lem  46602  ovnsubaddlem2  46608  hoidmvval0b  46627  hspdifhsp  46653  fsetprcnexALT  47092  uniimaelsetpreimafv  47426  imasetpreimafvbijlemfv1  47433  dfgric2  47945  gricuspgr  47948  gricsym  47951  grictr  47953  gricen  47955  dfgrlic2  48038  dfgrlic3  48040  grlicen  48047  gricgrlic  48048  usgrexmpl12ngric  48068  usgrexmpl12ngrlic  48069  opmpoismgm  48197  neircl  48935  sectrcl  49053  invrcl  49055  isorcl  49064  iinfssc  49088  iinfsubc  49089  imaid  49185  thincn0eu  49462  thinccic  49502  termcterm2  49545  eufunc  49553  euendfunc  49557  diag1f1o  49565  diag2f1o  49568  prstchom2ALT  49595  rellan  49654  relran  49655  alscn0d  49826