Theorem n0 4247

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 2177. (Revised by Gino Giotto, 28-Jun-2024.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1543  ∃wex 1787   ∈ wcel 2112   ≠ wne 2932  ∅c0 4223

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-ne 2933  df-dif 3856  df-nul 4224

This theorem is referenced by:  reximdva0  4252  rspn0  4253  rspn0OLD  4254  n0rex  4255  n0moeu  4257  eqeuel  4263  ndisj  4268  pssnel  4371  r19.2z  4392  r19.2zb  4393  r19.3rz  4394  uniintsn  4884  iunn0  4961  trintss  5163  intex  5215  notzfaus  5239  notzfausOLD  5240  reusv2lem1  5276  nnullss  5331  exss  5332  opabn0  5419  wefrc  5530  wereu2  5533  dmxp  5783  xpnz  6002  dmsnn0  6050  unixp0  6126  xpco  6132  frpomin  6172  onfr  6230  fveqdmss  6877  eldmrexrnb  6889  isofrlem  7127  limuni3  7609  soex  7677  f1oweALT  7723  fo1stres  7765  fo2ndres  7766  ecdmn0  8416  fsetprcnex  8521  map0g  8543  ixpn0  8589  resixpfo  8595  domdifsn  8706  xpdom3  8721  fodomr  8775  mapdom3  8796  findcard2OLD  8891  unblem2  8902  marypha1lem  9027  brwdom2  9167  unxpwdom2  9182  ixpiunwdom  9184  zfreg  9189  epfrs  9325  scott0  9467  cplem1  9470  fseqen  9606  finacn  9629  iunfictbso  9693  aceq2  9698  dfac3  9700  dfac9  9715  kmlem6  9734  kmlem8  9736  infpss  9796  fin23lem7  9895  enfin2i  9900  fin23lem21  9918  fin23lem31  9922  isf32lem9  9940  isf34lem4  9956  axdc2lem  10027  axdc3lem4  10032  ac6c4  10060  ac9  10062  ac6s4  10069  ac9s  10072  ttukeyg  10096  fpwwe2lem11  10220  wun0  10297  tsk0  10342  gruina  10397  genpn0  10582  prlem934  10612  ltaddpr  10613  ltexprlem1  10615  prlem936  10626  reclem2pr  10627  suplem1pr  10631  supsr  10691  axpre-sup  10748  dedekind  10960  dedekindle  10961  negn0  11226  infm3  11756  supaddc  11764  supadd  11765  supmul1  11766  supmullem2  11768  supmul  11769  zsupss  12498  xrsupsslem  12862  xrinfmsslem  12863  supxrre  12882  infxrre  12891  ixxub  12921  ixxlb  12922  ioorebas  13004  fzn0  13091  fzon0  13225  hashgt0elexb  13934  swrdcl  14175  pfxcl  14207  maxprmfct  16229  4sqlem12  16472  vdwmc  16494  ramz  16541  ramub1  16544  mreiincl  17053  mremre  17061  mreexexlem4d  17104  iscatd2  17138  catcone0  17144  cic  17258  drsdirfi  17766  opifismgm  18085  dfgrp3lem  18415  dfgrp3e  18417  issubg2  18512  subgint  18521  giclcl  18630  gicrcl  18631  gicsym  18632  gictr  18633  gicen  18635  gicsubgen  18636  cntzssv  18676  symggen  18816  psgnunilem3  18842  sylow1lem4  18944  odcau  18947  sylow3  18976  cyggex2  19236  giccyg  19239  pgpfac1lem5  19420  brric2  19719  subrgint  19776  lss0cl  19937  lmiclcl  20061  lmicrcl  20062  lmicsym  20063  lspsnat  20136  lspprat  20144  abvn0b  20294  cnsubrg  20377  cygzn  20489  lmiclbs  20753  lmisfree  20758  lmictra  20761  mpfrcl  20999  ply1frcl  21188  mdetdiaglem  21449  mdet0  21457  toponmre  21944  iunconnlem  22278  iunconn  22279  unconn  22280  clsconn  22281  2ndcdisj  22307  2ndcsep  22310  1stcelcls  22312  locfincmp  22377  comppfsc  22383  txcls  22455  hmphsym  22633  hmphtr  22634  hmphen  22636  haushmphlem  22638  cmphmph  22639  connhmph  22640  reghmph  22644  nrmhmph  22645  hmphdis  22647  hmphen2  22650  fbdmn0  22685  isfbas2  22686  fbssint  22689  trfbas2  22694  filtop  22706  isfil2  22707  elfg  22722  fgcl  22729  filssufilg  22762  uffix2  22775  ufildom1  22777  hauspwpwf1  22838  hausflf2  22849  alexsubALTlem2  22899  ptcmplem2  22904  cnextf  22917  tgptsmscld  23002  ustfilxp  23064  xbln0  23266  lpbl  23355  met2ndci  23374  metustfbas  23409  restmetu  23422  reconn  23679  opnreen  23682  metdsre  23704  phtpcer  23846  phtpc01  23847  phtpcco2  23850  pcohtpy  23871  cfilfcls  24125  cmetcaulem  24139  cmetcau  24140  bcthlem5  24179  ovolicc2lem2  24369  ovolicc2lem5  24372  ioorcl2  24423  ioorinv2  24426  itg11  24542  dvlip  24844  dvne0  24862  fta1g  25019  plyssc  25048  fta1  25155  vieta1lem2  25158  hpgerlem  26810  axcontlem4  27012  axcontlem10  27018  upgrex  27137  fusgrn0degnn0  27541  uhgrvd00  27576  wspthsnonn0vne  27955  eulerpath  28278  frgrwopreglem2  28350  ubthlem1  28905  shintcli  29364  2ndimaxp  30657  fpwrelmapffslem  30741  qsxpid  31226  qsidomlem2  31297  dimcl  31356  lvecdim0i  31357  lvecdim0  31358  lssdimle  31359  dimpropd  31360  dimkerim  31376  fedgmul  31380  extdg1id  31406  fmcncfil  31549  insiga  31771  unelldsys  31792  bnj521  32382  bnj1189  32656  bnj1279  32665  pconnconn  32860  txsconn  32870  cvmsss2  32903  cvmopnlem  32907  cvmfolem  32908  cvmliftmolem2  32911  cvmlift2lem10  32941  cvmliftpht  32947  cvmlift3lem8  32955  eldm3  33398  fundmpss  33410  elima4  33420  frmin  33459  nocvxmin  33659  sslttr  33687  sltlpss  33773  lrrecfr  33786  neibastop1  34234  neibastop2lem  34235  neibastop2  34236  fnemeet2  34242  fnejoin2  34244  neifg  34246  tailfb  34252  filnetlem3  34255  bj-n0i  34826  bj-rest10  34943  bj-restn0  34945  poimirlem30  35493  itg2addnclem2  35515  prdsbnd2  35639  heibor1lem  35653  bfp  35668  divrngidl  35872  rnxrn  36210  trcoss2  36288  atex  37106  llnn0  37216  lplnn0N  37247  lvoln0N  37291  pmapglb2N  37471  pmapglb2xN  37472  elpaddn0  37500  osumcllem8N  37663  pexmidlem5N  37674  diaglbN  38755  diaintclN  38758  dibglbN  38866  dibintclN  38867  dihglblem2aN  38993  dihglblem5  38998  dihglbcpreN  39000  dihintcl  39044  rencldnfilem  40286  kelac1  40532  lnmlmic  40557  gicabl  40568  neik0pk1imk0  41275  ntrneineine0lem  41311  scotteld  41478  onfrALT  41783  onfrALTVD  42125  iunconnlem2  42169  snelmap  42246  eliin2f  42268  disjinfi  42345  mapss2  42359  difmap  42361  infrpge  42504  infxrlesupxr  42590  inficc  42688  fsumnncl  42730  ellimciota  42773  islpcn  42798  lptre2pt  42799  stoweidlem35  43194  fourierdlem31  43297  fourier2  43386  qndenserrnbllem  43453  qndenserrnopn  43457  qndenserrn  43458  intsaluni  43486  sge0cl  43537  ovn0lem  43721  ovnsubaddlem2  43727  hoidmvval0b  43746  hspdifhsp  43772  fsetprcnexALT  44171  uniimaelsetpreimafv  44464  imasetpreimafvbijlemfv1  44471  mgmpropd  44945  opmpoismgm  44977  nzerooringczr  45246  neircl  45814  thincn0eu  45929  thinccic  45958  prstchom2ALT  45974  alscn0d  46113