Theorem n0 4313

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.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

Step	Hyp	Ref	Expression
1		nfcv 2980	. 2 ⊢ Ⅎ𝑥𝐴
2	1	n0f 4310	1 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:   ↔ wb 208  ∃wex 1779   ∈ wcel 2113   ≠ wne 3019  ∅c0 4294

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-dif 3942  df-nul 4295

This theorem is referenced by:  reximdva0  4315  rspn0  4316  n0rex  4317  n0moeu  4319  eqeuel  4325  ndisj  4330  pssnel  4423  r19.2z  4443  r19.2zb  4444  r19.3rz  4445  uniintsn  4916  iunn0  4992  trintss  5192  intex  5243  notzfaus  5265  notzfausOLD  5266  reusv2lem1  5302  nnullss  5357  exss  5358  opabn0  5443  wefrc  5552  wereu2  5555  dmxp  5802  xpnz  6019  dmsnn0  6067  unixp0  6137  xpco  6143  onfr  6233  fveqdmss  6849  eldmrexrnb  6861  isofrlem  7096  limuni3  7570  soex  7629  f1oweALT  7676  fo1stres  7718  fo2ndres  7719  ecdmn0  8339  map0g  8451  ixpn0  8497  resixpfo  8503  domdifsn  8603  xpdom3  8618  fodomr  8671  mapdom3  8692  findcard2  8761  unblem2  8774  marypha1lem  8900  brwdom2  9040  unxpwdom2  9055  ixpiunwdom  9058  zfreg  9062  epfrs  9176  scott0  9318  cplem1  9321  fseqen  9456  finacn  9479  iunfictbso  9543  aceq2  9548  dfac3  9550  dfac9  9565  kmlem6  9584  kmlem8  9586  infpss  9642  fin23lem7  9741  enfin2i  9746  fin23lem21  9764  fin23lem31  9768  isf32lem9  9786  isf34lem4  9802  axdc2lem  9873  axdc3lem4  9878  ac6c4  9906  ac9  9908  ac6s4  9915  ac9s  9918  ttukeyg  9942  fpwwe2lem12  10066  wun0  10143  tsk0  10188  gruina  10243  genpn0  10428  prlem934  10458  ltaddpr  10459  ltexprlem1  10461  prlem936  10472  reclem2pr  10473  suplem1pr  10477  supsr  10537  axpre-sup  10594  dedekind  10806  dedekindle  10807  negn0  11072  infm3  11603  supaddc  11611  supadd  11612  supmul1  11613  supmullem2  11615  supmul  11616  zsupss  12340  xrsupsslem  12703  xrinfmsslem  12704  supxrre  12723  infxrre  12732  ixxub  12762  ixxlb  12763  ioorebas  12842  fzn0  12924  fzon0  13058  hashgt0elexb  13766  swrdcl  14010  pfxcl  14042  maxprmfct  16056  4sqlem12  16295  vdwmc  16317  ramz  16364  ramub1  16367  mreiincl  16870  mremre  16878  mreexexlem4d  16921  iscatd2  16955  cic  17072  drsdirfi  17551  opifismgm  17872  dfgrp3lem  18200  dfgrp3e  18202  issubg2  18297  subgint  18306  giclcl  18415  gicrcl  18416  gicsym  18417  gictr  18418  gicen  18420  gicsubgen  18421  cntzssv  18461  symggen  18601  psgnunilem3  18627  sylow1lem4  18729  odcau  18732  sylow3  18761  cyggex2  19020  giccyg  19023  pgpfac1lem5  19204  brric2  19503  subrgint  19560  lss0cl  19721  lmiclcl  19845  lmicrcl  19846  lmicsym  19847  lspsnat  19920  lspprat  19928  abvn0b  20078  mpfrcl  20301  ply1frcl  20484  cnsubrg  20608  cygzn  20720  lmiclbs  20984  lmisfree  20989  lmictra  20992  mdetdiaglem  21210  mdet0  21218  toponmre  21704  iunconnlem  22038  iunconn  22039  unconn  22040  clsconn  22041  2ndcdisj  22067  2ndcsep  22070  1stcelcls  22072  locfincmp  22137  comppfsc  22143  txcls  22215  hmphsym  22393  hmphtr  22394  hmphen  22396  haushmphlem  22398  cmphmph  22399  connhmph  22400  reghmph  22404  nrmhmph  22405  hmphdis  22407  hmphen2  22410  fbdmn0  22445  isfbas2  22446  fbssint  22449  trfbas2  22454  filtop  22466  isfil2  22467  elfg  22482  fgcl  22489  filssufilg  22522  uffix2  22535  ufildom1  22537  hauspwpwf1  22598  hausflf2  22609  alexsubALTlem2  22659  ptcmplem2  22664  cnextf  22677  tgptsmscld  22762  ustfilxp  22824  xbln0  23027  lpbl  23116  met2ndci  23135  metustfbas  23170  restmetu  23183  reconn  23439  opnreen  23442  metdsre  23464  phtpcer  23602  phtpc01  23603  phtpcco2  23606  pcohtpy  23627  cfilfcls  23880  cmetcaulem  23894  cmetcau  23895  bcthlem5  23934  ovolicc2lem2  24122  ovolicc2lem5  24125  ioorcl2  24176  ioorinv2  24179  itg11  24295  dvlip  24593  dvne0  24611  fta1g  24764  plyssc  24793  fta1  24900  vieta1lem2  24903  hpgerlem  26554  axcontlem4  26756  axcontlem10  26762  upgrex  26880  fusgrn0degnn0  27284  uhgrvd00  27319  wspthsnonn0vne  27699  eulerpath  28023  frgrwopreglem2  28095  ubthlem1  28650  shintcli  29109  fpwrelmapffslem  30471  qsxpid  30931  qsidomlem2  30970  dimcl  31007  lvecdim0i  31008  lvecdim0  31009  lssdimle  31010  dimpropd  31011  dimkerim  31027  fedgmul  31031  extdg1id  31057  fmcncfil  31178  insiga  31400  unelldsys  31421  bnj521  32011  bnj1189  32285  bnj1279  32294  pconnconn  32482  txsconn  32492  cvmsss2  32525  cvmopnlem  32529  cvmfolem  32530  cvmliftmolem2  32533  cvmlift2lem10  32563  cvmliftpht  32569  cvmlift3lem8  32577  eldm3  33001  fundmpss  33013  elima4  33023  frpomin  33082  frmin  33088  nocvxmin  33252  sslttr  33272  neibastop1  33711  neibastop2lem  33712  neibastop2  33713  fnemeet2  33719  fnejoin2  33721  neifg  33723  tailfb  33729  filnetlem3  33732  bj-n0i  34266  bj-rest10  34383  bj-restn0  34385  poimirlem30  34926  itg2addnclem2  34948  prdsbnd2  35077  heibor1lem  35091  bfp  35106  divrngidl  35310  rnxrn  35650  trcoss2  35728  atex  36546  llnn0  36656  lplnn0N  36687  lvoln0N  36731  pmapglb2N  36911  pmapglb2xN  36912  elpaddn0  36940  osumcllem8N  37103  pexmidlem5N  37114  diaglbN  38195  diaintclN  38198  dibglbN  38306  dibintclN  38307  dihglblem2aN  38433  dihglblem5  38438  dihglbcpreN  38440  dihintcl  38484  rencldnfilem  39423  kelac1  39669  lnmlmic  39694  gicabl  39705  neik0pk1imk0  40403  ntrneineine0lem  40439  scotteld  40588  onfrALT  40889  onfrALTVD  41231  iunconnlem2  41275  snelmap  41352  eliin2f  41376  suprnmpt  41436  disjinfi  41460  mapss2  41474  difmap  41476  infrpge  41625  infxrlesupxr  41716  inficc  41816  fsumnncl  41858  ellimciota  41901  islpcn  41926  lptre2pt  41927  stoweidlem35  42327  fourierdlem31  42430  fourier2  42519  qndenserrnbllem  42586  qndenserrnopn  42590  qndenserrn  42591  intsaluni  42619  sge0cl  42670  ovn0lem  42854  ovnsubaddlem2  42860  hoidmvval0b  42879  hspdifhsp  42905  uniimaelsetpreimafv  43563  imasetpreimafvbijlemfv1  43570  mgmpropd  44049  opmpoismgm  44081  nzerooringczr  44350  alscn0d  44903