Theorem n0 4288

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 207   = wceq 1547  ∃wex 1786   ∈ wcel 2119   ≠ wne 2935  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-ne 2936  df-dif 3893  df-nul 4269

This theorem is referenced by:  reximdva0  4290  rspn0  4291  n0rex  4292  n0moeu  4294  eqeuel  4300  ndisj  4305  pssnel  4406  r19.2z  4434  r19.3rz  4436  uniintsn  4922  iunn0  5003  trintss  5205  intex  5279  notzfaus  5299  reusv2lem1  5334  nnullss  5408  exss  5409  opabn0  5502  wefrc  5619  wereu2  5622  dmxp  5878  xpnz  6117  dmsnn0  6165  unixp0  6241  xpco  6247  frpomin  6298  onfr  6356  iotanul2  6465  fveqdmss  7026  eldmrexrnb  7040  isofrlem  7291  limuni3  7799  soex  7868  f1oweALT  7921  fo1stres  7964  fo2ndres  7965  ecdmn0  8693  fsetprcnex  8806  map0g  8829  ixpn0  8875  resixpfo  8881  domdifsn  8995  xpdom3  9010  fodomr  9063  mapdom3  9084  0sdom1dom  9153  unblem2  9200  fodomfir  9235  marypha1lem  9343  brwdom2  9485  unxpwdom2  9500  ixpiunwdom  9502  zfreg  9508  epfrs  9650  frmin  9671  scott0  9808  cplem1  9811  fseqen  9947  finacn  9970  iunfictbso  10034  aceq2  10039  dfac3  10041  dfac9  10057  kmlem6  10076  kmlem8  10078  infpss  10136  fin23lem7  10236  enfin2i  10241  fin23lem21  10259  fin23lem31  10263  isf32lem9  10281  isf34lem4  10297  axdc2lem  10368  axdc3lem4  10373  ac6c4  10401  ac9  10403  ac6s4  10410  ac9s  10413  ttukeyg  10437  fpwwe2lem11  10562  wun0  10639  tsk0  10684  gruina  10739  genpn0  10924  prlem934  10954  ltaddpr  10955  ltexprlem1  10957  prlem936  10968  reclem2pr  10969  suplem1pr  10973  supsr  11033  axpre-sup  11090  dedekind  11307  dedekindle  11308  negn0  11577  infm3  12113  supaddc  12121  supadd  12122  supmul1  12123  supmullem2  12125  supmul  12126  zsupss  12885  xrsupsslem  13257  xrinfmsslem  13258  supxrre  13277  infxrre  13287  ixxub  13317  ixxlb  13318  ioorebas  13402  fzn0  13490  fzon0  13630  hashgt0elexb  14362  swrdcl  14606  pfxcl  14638  maxprmfct  16677  4sqlem12  16925  vdwmc  16947  ramz  16994  ramub1  16997  mreiincl  17556  mremre  17564  mreexexlem4d  17611  iscatd2  17645  catcone0  17651  cic  17764  drsdirfi  18269  mgmpropd  18617  opifismgm  18625  dfgrp3lem  19012  dfgrp3e  19014  issubg2  19115  subgint  19124  giclcl  19246  gicrcl  19247  gicsym  19248  gictr  19249  gicen  19251  gicsubgen  19252  cntzssv  19301  symggen  19443  psgnunilem3  19469  sylow1lem4  19574  odcau  19577  sylow3  19606  cyggex2  19870  giccyg  19873  pgpfac1lem5  20054  ricsym  20484  brric2  20485  subrngint  20539  subrgint  20574  abvn0b  20815  lss0cl  20944  lmiclcl  21067  lmicrcl  21068  lmicsym  21069  lspsnat  21145  lspprat  21153  cnsubrg  21409  nzerooringczr  21462  cygzn  21552  lmiclbs  21819  lmisfree  21824  lmictra  21827  mpfrcl  22068  ply1frcl  22311  mdetdiaglem  22588  mdet0  22596  toponmre  23083  iunconnlem  23417  iunconn  23418  unconn  23419  clsconn  23420  2ndcdisj  23446  2ndcsep  23449  1stcelcls  23451  locfincmp  23516  comppfsc  23522  txcls  23594  hmphsym  23772  hmphtr  23773  hmphen  23775  haushmphlem  23777  cmphmph  23778  connhmph  23779  reghmph  23783  nrmhmph  23784  hmphdis  23786  hmphen2  23789  fbdmn0  23824  isfbas2  23825  fbssint  23828  trfbas2  23833  filtop  23845  isfil2  23846  elfg  23861  fgcl  23868  filssufilg  23901  uffix2  23914  ufildom1  23916  hauspwpwf1  23977  hausflf2  23988  alexsubALTlem2  24038  ptcmplem2  24043  cnextf  24056  tgptsmscld  24141  ustfilxp  24203  xbln0  24404  lpbl  24493  met2ndci  24512  metustfbas  24547  restmetu  24560  reconn  24819  opnreen  24822  metdsre  24844  phtpcer  24987  phtpc01  24988  phtpcco2  24991  pcohtpy  25012  cfilfcls  25266  cmetcaulem  25280  cmetcau  25281  bcthlem5  25320  ovolicc2lem2  25510  ovolicc2lem5  25513  ioorcl2  25564  ioorinv2  25567  itg11  25683  dvlip  25985  dvne0  26003  fta1g  26160  plyssc  26190  fta1  26299  vieta1lem2  26302  nobdaymin  27770  sltstr  27804  ltslpss  27925  lrrecfr  27960  oncutlt  28281  hpgerlem  28858  axcontlem4  29061  axcontlem10  29067  upgrex  29186  fusgrn0degnn0  29593  uhgrvd00  29628  wspthsnonn0vne  30010  eulerpath  30336  frgrwopreglem2  30408  ubthlem1  30966  shintcli  31425  n0limd  32566  2ndimaxp  32745  fpwrelmapffslem  32831  qsxpid  33452  qsidomlem2  33543  qsdrng  33587  1arithidom  33627  dimcl  33794  lmimdim  33795  lmicdim  33796  lvecdim0i  33797  lvecdim0  33798  lssdimle  33799  dimpropd  33800  dimkerim  33818  fedgmul  33822  extdg1id  33857  fmcncfil  34122  insiga  34328  unelldsys  34349  bnj1189  35198  bnj1279  35207  axregszf  35317  pconnconn  35466  txsconn  35476  cvmsss2  35509  cvmopnlem  35513  cvmfolem  35514  cvmliftmolem2  35517  cvmlift2lem10  35547  cvmliftpht  35553  cvmlift3lem8  35561  eldm3  35996  fundmpss  36002  elima4  36011  neibastop1  36594  neibastop2lem  36595  neibastop2  36596  fnemeet2  36602  fnejoin2  36604  neifg  36606  tailfb  36612  filnetlem3  36615  mh-infprim1bi  36781  bj-n0i  37311  bj-rest10  37453  bj-restn0  37455  poimirlem30  38024  itg2addnclem2  38046  prdsbnd2  38169  heibor1lem  38183  bfp  38198  divrngidl  38402  eldmres3  38657  rnxrn  38795  eldmxrncnvepres2  38809  trcoss2  38948  atex  39905  llnn0  40015  lplnn0N  40046  lvoln0N  40090  pmapglb2N  40270  pmapglb2xN  40271  elpaddn0  40299  osumcllem8N  40462  pexmidlem5N  40473  diaglbN  41554  diaintclN  41557  dibglbN  41665  dibintclN  41666  dihglblem2aN  41792  dihglblem5  41797  dihglbcpreN  41799  dihintcl  41843  unitscyglem5  42691  rictr  43013  riccrng1  43014  ricdrng1  43021  rencldnfilem  43272  kelac1  43515  lnmlmic  43540  gicabl  43551  neik0pk1imk0  44498  ntrneineine0lem  44534  scotteld  44697  onfrALT  45000  onfrALTVD  45341  iunconnlem2  45385  relpfrlem  45404  dfac5prim  45441  permac8prim  45465  snelmap  45537  eliin2f  45558  disjinfi  45646  mapss2  45658  difmap  45659  infrpge  45803  infxrlesupxr  45886  inficc  45986  fsumnncl  46024  ellimciota  46066  islpcn  46089  lptre2pt  46090  stoweidlem35  46485  fourierdlem31  46588  fourier2  46677  qndenserrnbllem  46744  qndenserrnopn  46748  qndenserrn  46749  intsaluni  46779  sge0cl  46831  ovn0lem  47015  ovnsubaddlem2  47021  hoidmvval0b  47040  hspdifhsp  47066  fsetprcnexALT  47532  uniimaelsetpreimafv  47878  imasetpreimafvbijlemfv1  47885  dfgric2  48413  gricuspgr  48416  gricsym  48419  grictr  48421  gricen  48423  dfgrlic2  48506  dfgrlic3  48508  grlicen  48515  gricgrlic  48516  usgrexmpl12ngric  48536  usgrexmpl12ngrlic  48537  opmpoismgm  48665  neircl  49402  sectrcl  49519  invrcl  49521  isorcl  49530  iinfssc  49554  iinfsubc  49555  imaid  49651  thincn0eu  49928  thinccic  49968  termcterm2  50011  eufunc  50019  euendfunc  50023  diag1f1o  50031  diag2f1o  50034  prstchom2ALT  50061  rellan  50120  relran  50121  alscn0d  50292