Theorem n0 4132

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 2948	. 2 ⊢ Ⅎ𝑥𝐴
2	1	n0f 4129	1 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

Syntax hints:   ↔ wb 197  ∃wex 1859   ∈ wcel 2156   ≠ wne 2978  ∅c0 4116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-v 3393  df-dif 3772  df-nul 4117

This theorem is referenced by:  reximdva0  4134  rspn0  4135  n0rex  4136  n0moeu  4138  eqeuel  4142  pssnel  4235  r19.2z  4255  r19.2zb  4256  r19.3rz  4257  uniintsn  4706  iunn0  4772  trintss  4962  intex  5012  notzfaus  5032  reusv2lem1  5067  nnullss  5120  exss  5121  opabn0  5201  wefrc  5305  wereu2  5308  dmxp  5545  xpnz  5764  dmsnn0  5811  unixp0  5883  xpco  5889  onfr  5975  fveqdmss  6572  eldmrexrnb  6584  isofrlem  6810  limuni3  7278  soex  7335  f1oweALT  7378  fo1stres  7420  fo2ndres  7421  ecdmn0  8020  map0g  8129  ixpn0  8173  resixpfo  8179  domdifsn  8278  xpdom3  8293  fodomr  8346  mapdom3  8367  findcard2  8435  unblem2  8448  marypha1lem  8574  brwdom2  8713  unxpwdom2  8728  ixpiunwdom  8731  zfreg  8735  epfrs  8850  scott0  8992  cplem1  8995  fseqen  9129  finacn  9152  iunfictbso  9216  aceq2  9221  dfac3  9223  dfac9  9239  kmlem6  9258  kmlem8  9260  infpss  9320  fin23lem7  9419  enfin2i  9424  fin23lem21  9442  fin23lem31  9446  isf32lem9  9464  isf34lem4  9480  axdc2lem  9551  axdc3lem4  9556  ac6c4  9584  ac9  9586  ac6s4  9593  ac9s  9596  ttukeyg  9620  fpwwe2lem12  9744  wun0  9821  tsk0  9866  gruina  9921  genpn0  10106  prlem934  10136  ltaddpr  10137  ltexprlem1  10139  prlem936  10150  reclem2pr  10151  suplem1pr  10155  supsr  10214  axpre-sup  10271  dedekind  10481  dedekindle  10482  negn0  10740  infm3  11263  supaddc  11271  supadd  11272  supmul1  11273  supmullem2  11275  supmul  11276  zsupss  11992  xrsupsslem  12351  xrinfmsslem  12352  supxrre  12371  infxrre  12380  ixxub  12410  ixxlb  12411  ioorebas  12490  fzn0  12574  fzon0  12707  hashgt0elexb  13403  swrdcl  13638  xpcogend  13934  maxprmfct  15634  4sqlem12  15873  vdwmc  15895  ramz  15942  ramub1  15945  mreiincl  16457  mremre  16465  mreexexlem4d  16508  iscatd2  16542  cic  16659  drsdirfi  17139  opifismgm  17459  dfgrp3lem  17714  dfgrp3e  17716  issubg2  17807  subgint  17816  giclcl  17912  gicrcl  17913  gicsym  17914  gictr  17915  gicen  17917  gicsubgen  17918  cntzssv  17958  symggen  18087  psgnunilem3  18113  sylow1lem4  18213  odcau  18216  sylow3  18245  cyggex2  18495  giccyg  18498  pgpfac1lem5  18676  brric2  18945  subrgint  19002  lss0cl  19147  lmiclcl  19273  lmicrcl  19274  lmicsym  19275  lspsnat  19349  lspprat  19358  abvn0b  19507  mpfrcl  19722  ply1frcl  19887  cnsubrg  20010  cygzn  20122  lmiclbs  20383  lmisfree  20388  lmictra  20391  mdetdiaglem  20612  mdet0  20620  toponmre  21108  iunconnlem  21441  iunconn  21442  unconn  21443  clsconn  21444  2ndcdisj  21470  2ndcsep  21473  1stcelcls  21475  locfincmp  21540  comppfsc  21546  txcls  21618  hmphsym  21796  hmphtr  21797  hmphen  21799  haushmphlem  21801  cmphmph  21802  connhmph  21803  reghmph  21807  nrmhmph  21808  hmphdis  21810  hmphen2  21813  fbdmn0  21848  isfbas2  21849  fbssint  21852  trfbas2  21857  filtop  21869  isfil2  21870  elfg  21885  fgcl  21892  filssufilg  21925  uffix2  21938  ufildom1  21940  hauspwpwf1  22001  hausflf2  22012  alexsubALTlem2  22062  ptcmplem2  22067  cnextf  22080  tgptsmscld  22164  ustfilxp  22226  xbln0  22429  lpbl  22518  met2ndci  22537  metustfbas  22572  restmetu  22585  reconn  22841  opnreen  22844  metdsre  22866  phtpcer  23004  phtpc01  23005  phtpcco2  23008  pcohtpy  23029  cfilfcls  23282  cmetcaulem  23296  cmetcau  23297  cmetss  23323  bcthlem5  23335  ovolicc2lem2  23498  ovolicc2lem5  23501  ioorcl2  23552  ioorinv2  23555  itg11  23671  dvlip  23969  dvne0  23987  fta1g  24140  plyssc  24169  fta1  24276  vieta1lem2  24279  hpgerlem  25870  axcontlem4  26060  axcontlem10  26066  upgrex  26200  fusgrn0degnn0  26622  uhgrvd00  26657  wspthsnonn0vne  27056  eulerpath  27413  frgrwopreglem2  27487  ubthlem1  28053  shintcli  28515  fpwrelmapffslem  29833  fmcncfil  30301  insiga  30524  unelldsys  30545  bnj521  31127  bnj1189  31398  bnj1279  31407  pconnconn  31534  txsconn  31544  cvmsss2  31577  cvmopnlem  31581  cvmfolem  31582  cvmliftmolem2  31585  cvmlift2lem10  31615  cvmliftpht  31621  cvmlift3lem8  31629  eldm3  31971  fundmpss  31984  elima4  31997  frpomin  32057  frmin  32061  nocvxmin  32213  sslttr  32233  neibastop1  32673  neibastop2lem  32674  neibastop2  32675  fnemeet2  32681  fnejoin2  32683  neifg  32685  tailfb  32691  filnetlem3  32694  bj-n0i  33244  bj-rest10  33350  bj-restn0  33352  poimirlem30  33750  itg2addnclem2  33772  prdsbnd2  33903  heibor1lem  33917  bfp  33932  divrngidl  34136  rnxrn  34467  trcoss2  34545  atex  35184  llnn0  35294  lplnn0N  35325  lvoln0N  35369  pmapglb2N  35549  pmapglb2xN  35550  elpaddn0  35578  osumcllem8N  35741  pexmidlem5N  35752  diaglbN  36833  diaintclN  36836  dibglbN  36944  dibintclN  36945  dihglblem2aN  37071  dihglblem5  37076  dihglbcpreN  37078  dihintcl  37122  rencldnfilem  37883  kelac1  38131  lnmlmic  38156  gicabl  38167  ndisj  38560  neik0pk1imk0  38842  ntrneineine0lem  38878  onfrALT  39259  onfrALTVD  39618  iunconnlem2  39662  snelmap  39744  eliin2f  39776  suprnmpt  39841  disjinfi  39866  mapss2  39881  difmap  39883  infrpge  40044  infxrlesupxr  40139  inficc  40238  fsumnncl  40280  ellimciota  40323  islpcn  40348  lptre2pt  40349  stoweidlem35  40728  fourierdlem31  40831  fourier2  40920  qndenserrnbllem  40990  qndenserrnopn  40994  qndenserrn  40995  intsaluni  41023  sge0cl  41074  ovn0lem  41258  ovnsubaddlem2  41264  hoidmvval0b  41283  hspdifhsp  41309  pfxcl  41958  mgmpropd  42340  opmpt2ismgm  42372  nzerooringczr  42637  alscn0d  43109