Theorem n0 4236

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

Syntax hints:   ↔ wb 207  ∃wex 1765   ∈ wcel 2083   ≠ wne 2986  ∅c0 4217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-dif 3868  df-nul 4218

This theorem is referenced by:  reximdva0  4238  rspn0  4239  n0rex  4240  n0moeu  4242  eqeuel  4248  ndisj  4253  pssnel  4340  r19.2z  4360  r19.2zb  4361  r19.3rz  4362  uniintsn  4825  iunn0  4894  trintss  5087  intex  5138  notzfaus  5160  notzfausOLD  5161  reusv2lem1  5197  nnullss  5253  exss  5254  opabn0  5335  wefrc  5444  wereu2  5447  dmxp  5688  xpnz  5899  dmsnn0  5946  unixp0  6016  xpco  6022  onfr  6112  fveqdmss  6718  eldmrexrnb  6730  isofrlem  6963  limuni3  7430  soex  7489  f1oweALT  7536  fo1stres  7578  fo2ndres  7579  ecdmn0  8193  map0g  8305  ixpn0  8349  resixpfo  8355  domdifsn  8454  xpdom3  8469  fodomr  8522  mapdom3  8543  findcard2  8611  unblem2  8624  marypha1lem  8750  brwdom2  8890  unxpwdom2  8905  ixpiunwdom  8908  zfreg  8912  epfrs  9026  scott0  9168  cplem1  9171  fseqen  9306  finacn  9329  iunfictbso  9393  aceq2  9398  dfac3  9400  dfac9  9415  kmlem6  9434  kmlem8  9436  infpss  9492  fin23lem7  9591  enfin2i  9596  fin23lem21  9614  fin23lem31  9618  isf32lem9  9636  isf34lem4  9652  axdc2lem  9723  axdc3lem4  9728  ac6c4  9756  ac9  9758  ac6s4  9765  ac9s  9768  ttukeyg  9792  fpwwe2lem12  9916  wun0  9993  tsk0  10038  gruina  10093  genpn0  10278  prlem934  10308  ltaddpr  10309  ltexprlem1  10311  prlem936  10322  reclem2pr  10323  suplem1pr  10327  supsr  10387  axpre-sup  10444  dedekind  10656  dedekindle  10657  negn0  10923  infm3  11454  supaddc  11462  supadd  11463  supmul1  11464  supmullem2  11466  supmul  11467  zsupss  12190  xrsupsslem  12554  xrinfmsslem  12555  supxrre  12574  infxrre  12583  ixxub  12613  ixxlb  12614  ioorebas  12693  fzn0  12775  fzon0  12909  hashgt0elexb  13615  swrdcl  13847  pfxcl  13879  maxprmfct  15886  4sqlem12  16125  vdwmc  16147  ramz  16194  ramub1  16197  mreiincl  16700  mremre  16708  mreexexlem4d  16751  iscatd2  16785  cic  16902  drsdirfi  17381  opifismgm  17701  dfgrp3lem  17958  dfgrp3e  17960  issubg2  18052  subgint  18061  giclcl  18157  gicrcl  18158  gicsym  18159  gictr  18160  gicen  18162  gicsubgen  18163  cntzssv  18203  symggen  18333  psgnunilem3  18359  sylow1lem4  18460  odcau  18463  sylow3  18492  cyggex2  18742  giccyg  18745  pgpfac1lem5  18922  brric2  19194  subrgint  19251  lss0cl  19412  lmiclcl  19536  lmicrcl  19537  lmicsym  19538  lspsnat  19611  lspprat  19619  abvn0b  19768  mpfrcl  19989  ply1frcl  20168  cnsubrg  20291  cygzn  20403  lmiclbs  20667  lmisfree  20672  lmictra  20675  mdetdiaglem  20895  mdet0  20903  toponmre  21389  iunconnlem  21723  iunconn  21724  unconn  21725  clsconn  21726  2ndcdisj  21752  2ndcsep  21755  1stcelcls  21757  locfincmp  21822  comppfsc  21828  txcls  21900  hmphsym  22078  hmphtr  22079  hmphen  22081  haushmphlem  22083  cmphmph  22084  connhmph  22085  reghmph  22089  nrmhmph  22090  hmphdis  22092  hmphen2  22095  fbdmn0  22130  isfbas2  22131  fbssint  22134  trfbas2  22139  filtop  22151  isfil2  22152  elfg  22167  fgcl  22174  filssufilg  22207  uffix2  22220  ufildom1  22222  hauspwpwf1  22283  hausflf2  22294  alexsubALTlem2  22344  ptcmplem2  22349  cnextf  22362  tgptsmscld  22446  ustfilxp  22508  xbln0  22711  lpbl  22800  met2ndci  22819  metustfbas  22854  restmetu  22867  reconn  23123  opnreen  23126  metdsre  23148  phtpcer  23286  phtpc01  23287  phtpcco2  23290  pcohtpy  23311  cfilfcls  23564  cmetcaulem  23578  cmetcau  23579  bcthlem5  23618  ovolicc2lem2  23806  ovolicc2lem5  23809  ioorcl2  23860  ioorinv2  23863  itg11  23979  dvlip  24277  dvne0  24295  fta1g  24448  plyssc  24477  fta1  24584  vieta1lem2  24587  hpgerlem  26237  axcontlem4  26440  axcontlem10  26446  upgrex  26564  fusgrn0degnn0  26968  uhgrvd00  27003  wspthsnonn0vne  27382  eulerpath  27706  frgrwopreglem2  27780  ubthlem1  28334  shintcli  28793  fpwrelmapffslem  30152  dimcl  30603  lvecdim0i  30604  lvecdim0  30605  lssdimle  30606  dimpropd  30607  dimkerim  30623  fedgmul  30627  extdg1id  30653  fmcncfil  30787  insiga  31009  unelldsys  31030  bnj521  31620  bnj1189  31891  bnj1279  31900  pconnconn  32088  txsconn  32098  cvmsss2  32131  cvmopnlem  32135  cvmfolem  32136  cvmliftmolem2  32139  cvmlift2lem10  32169  cvmliftpht  32175  cvmlift3lem8  32183  eldm3  32607  fundmpss  32619  elima4  32629  frpomin  32689  frmin  32695  nocvxmin  32859  sslttr  32879  neibastop1  33318  neibastop2lem  33319  neibastop2  33320  fnemeet2  33326  fnejoin2  33328  neifg  33330  tailfb  33336  filnetlem3  33339  bj-n0i  33839  bj-rest10  33999  bj-restn0  34001  poimirlem30  34474  itg2addnclem2  34496  prdsbnd2  34626  heibor1lem  34640  bfp  34655  divrngidl  34859  rnxrn  35198  trcoss2  35276  atex  36094  llnn0  36204  lplnn0N  36235  lvoln0N  36279  pmapglb2N  36459  pmapglb2xN  36460  elpaddn0  36488  osumcllem8N  36651  pexmidlem5N  36662  diaglbN  37743  diaintclN  37746  dibglbN  37854  dibintclN  37855  dihglblem2aN  37981  dihglblem5  37986  dihglbcpreN  37988  dihintcl  38032  rencldnfilem  38923  kelac1  39169  lnmlmic  39194  gicabl  39205  neik0pk1imk0  39903  ntrneineine0lem  39939  scotteld  40100  onfrALT  40443  onfrALTVD  40785  iunconnlem2  40829  snelmap  40906  eliin2f  40931  suprnmpt  40991  disjinfi  41015  mapss2  41029  difmap  41031  infrpge  41181  infxrlesupxr  41273  inficc  41373  fsumnncl  41415  ellimciota  41458  islpcn  41483  lptre2pt  41484  stoweidlem35  41884  fourierdlem31  41987  fourier2  42076  qndenserrnbllem  42143  qndenserrnopn  42147  qndenserrn  42148  intsaluni  42176  sge0cl  42227  ovn0lem  42411  ovnsubaddlem2  42417  hoidmvval0b  42436  hspdifhsp  42462  mgmpropd  43546  opmpoismgm  43578  nzerooringczr  43843  alscn0d  44398