Theorem n0 4353

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ≠ wne 2940  ∅c0 4333

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 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-ne 2941  df-dif 3954  df-nul 4334

This theorem is referenced by:  reximdva0  4355  rspn0  4356  n0rex  4357  n0moeu  4359  eqeuel  4365  ndisj  4370  pssnel  4471  r19.2z  4495  r19.2zb  4496  r19.3rz  4497  uniintsn  4985  iunn0  5067  trintss  5278  intex  5344  notzfaus  5363  reusv2lem1  5398  nnullss  5467  exss  5468  opabn0  5558  wefrc  5679  wereu2  5682  dmxp  5939  dmxpOLD  5940  xpnz  6179  dmsnn0  6227  unixp0  6303  xpco  6309  frpomin  6361  onfr  6423  iotanul2  6531  fveqdmss  7098  eldmrexrnb  7112  isofrlem  7360  limuni3  7873  soex  7943  f1oweALT  7997  fo1stres  8040  fo2ndres  8041  ecdmn0  8794  fsetprcnex  8902  map0g  8924  ixpn0  8970  resixpfo  8976  domdifsn  9094  xpdom3  9110  fodomr  9168  mapdom3  9189  0sdom1dom  9274  unblem2  9329  fodomfir  9368  marypha1lem  9473  brwdom2  9613  unxpwdom2  9628  ixpiunwdom  9630  zfreg  9635  epfrs  9771  frmin  9789  scott0  9926  cplem1  9929  fseqen  10067  finacn  10090  iunfictbso  10154  aceq2  10159  dfac3  10161  dfac9  10177  kmlem6  10196  kmlem8  10198  infpss  10256  fin23lem7  10356  enfin2i  10361  fin23lem21  10379  fin23lem31  10383  isf32lem9  10401  isf34lem4  10417  axdc2lem  10488  axdc3lem4  10493  ac6c4  10521  ac9  10523  ac6s4  10530  ac9s  10533  ttukeyg  10557  fpwwe2lem11  10681  wun0  10758  tsk0  10803  gruina  10858  genpn0  11043  prlem934  11073  ltaddpr  11074  ltexprlem1  11076  prlem936  11087  reclem2pr  11088  suplem1pr  11092  supsr  11152  axpre-sup  11209  dedekind  11424  dedekindle  11425  negn0  11692  infm3  12227  supaddc  12235  supadd  12236  supmul1  12237  supmullem2  12239  supmul  12240  zsupss  12979  xrsupsslem  13349  xrinfmsslem  13350  supxrre  13369  infxrre  13378  ixxub  13408  ixxlb  13409  ioorebas  13491  fzn0  13578  fzon0  13717  hashgt0elexb  14441  swrdcl  14683  pfxcl  14715  maxprmfct  16746  4sqlem12  16994  vdwmc  17016  ramz  17063  ramub1  17066  mreiincl  17639  mremre  17647  mreexexlem4d  17690  iscatd2  17724  catcone0  17730  cic  17843  drsdirfi  18351  mgmpropd  18664  opifismgm  18672  dfgrp3lem  19056  dfgrp3e  19058  issubg2  19159  subgint  19168  giclcl  19291  gicrcl  19292  gicsym  19293  gictr  19294  gicen  19296  gicsubgen  19297  cntzssv  19346  symggen  19488  psgnunilem3  19514  sylow1lem4  19619  odcau  19622  sylow3  19651  cyggex2  19915  giccyg  19918  pgpfac1lem5  20099  brric2  20506  subrngint  20560  subrgint  20595  abvn0b  20837  lss0cl  20945  lmiclcl  21069  lmicrcl  21070  lmicsym  21071  lspsnat  21147  lspprat  21155  cnsubrg  21445  nzerooringczr  21491  cygzn  21589  lmiclbs  21857  lmisfree  21862  lmictra  21865  mpfrcl  22109  ply1frcl  22322  mdetdiaglem  22604  mdet0  22612  toponmre  23101  iunconnlem  23435  iunconn  23436  unconn  23437  clsconn  23438  2ndcdisj  23464  2ndcsep  23467  1stcelcls  23469  locfincmp  23534  comppfsc  23540  txcls  23612  hmphsym  23790  hmphtr  23791  hmphen  23793  haushmphlem  23795  cmphmph  23796  connhmph  23797  reghmph  23801  nrmhmph  23802  hmphdis  23804  hmphen2  23807  fbdmn0  23842  isfbas2  23843  fbssint  23846  trfbas2  23851  filtop  23863  isfil2  23864  elfg  23879  fgcl  23886  filssufilg  23919  uffix2  23932  ufildom1  23934  hauspwpwf1  23995  hausflf2  24006  alexsubALTlem2  24056  ptcmplem2  24061  cnextf  24074  tgptsmscld  24159  ustfilxp  24221  xbln0  24424  lpbl  24516  met2ndci  24535  metustfbas  24570  restmetu  24583  reconn  24850  opnreen  24853  metdsre  24875  phtpcer  25027  phtpc01  25028  phtpcco2  25032  pcohtpy  25053  cfilfcls  25308  cmetcaulem  25322  cmetcau  25323  bcthlem5  25362  ovolicc2lem2  25553  ovolicc2lem5  25556  ioorcl2  25607  ioorinv2  25610  itg11  25726  dvlip  26032  dvne0  26050  fta1g  26209  plyssc  26239  fta1  26350  vieta1lem2  26353  nocvxmin  27823  sslttr  27852  sltlpss  27945  lrrecfr  27976  hpgerlem  28773  axcontlem4  28982  axcontlem10  28988  upgrex  29109  fusgrn0degnn0  29517  uhgrvd00  29552  wspthsnonn0vne  29937  eulerpath  30260  frgrwopreglem2  30332  ubthlem1  30889  shintcli  31348  n0limd  32491  2ndimaxp  32656  fpwrelmapffslem  32743  qsxpid  33390  qsidomlem2  33481  qsdrng  33525  1arithidom  33565  dimcl  33653  lmimdim  33654  lmicdim  33655  lvecdim0i  33656  lvecdim0  33657  lssdimle  33658  dimpropd  33659  dimkerim  33678  fedgmul  33682  extdg1id  33716  fmcncfil  33930  insiga  34138  unelldsys  34159  bnj1189  35023  bnj1279  35032  pconnconn  35236  txsconn  35246  cvmsss2  35279  cvmopnlem  35283  cvmfolem  35284  cvmliftmolem2  35287  cvmlift2lem10  35317  cvmliftpht  35323  cvmlift3lem8  35331  eldm3  35761  fundmpss  35767  elima4  35776  neibastop1  36360  neibastop2lem  36361  neibastop2  36362  fnemeet2  36368  fnejoin2  36370  neifg  36372  tailfb  36378  filnetlem3  36381  bj-n0i  36952  bj-rest10  37089  bj-restn0  37091  poimirlem30  37657  itg2addnclem2  37679  prdsbnd2  37802  heibor1lem  37816  bfp  37831  divrngidl  38035  rnxrn  38399  trcoss2  38485  atex  39408  llnn0  39518  lplnn0N  39549  lvoln0N  39593  pmapglb2N  39773  pmapglb2xN  39774  elpaddn0  39802  osumcllem8N  39965  pexmidlem5N  39976  diaglbN  41057  diaintclN  41060  dibglbN  41168  dibintclN  41169  dihglblem2aN  41295  dihglblem5  41300  dihglbcpreN  41302  dihintcl  41346  unitscyglem5  42200  ricsym  42529  rictr  42530  riccrng1  42531  ricdrng1  42538  rencldnfilem  42831  kelac1  43075  lnmlmic  43100  gicabl  43111  neik0pk1imk0  44060  ntrneineine0lem  44096  scotteld  44265  onfrALT  44569  onfrALTVD  44911  iunconnlem2  44955  relpfrlem  44974  dfac5prim  45007  snelmap  45087  eliin2f  45109  disjinfi  45197  mapss2  45210  difmap  45212  infrpge  45362  infxrlesupxr  45447  inficc  45547  fsumnncl  45587  ellimciota  45629  islpcn  45654  lptre2pt  45655  stoweidlem35  46050  fourierdlem31  46153  fourier2  46242  qndenserrnbllem  46309  qndenserrnopn  46313  qndenserrn  46314  intsaluni  46344  sge0cl  46396  ovn0lem  46580  ovnsubaddlem2  46586  hoidmvval0b  46605  hspdifhsp  46631  fsetprcnexALT  47074  uniimaelsetpreimafv  47383  imasetpreimafvbijlemfv1  47390  dfgric2  47884  gricuspgr  47887  gricsym  47890  grictr  47892  gricen  47894  dfgrlic2  47968  dfgrlic3  47970  grlicen  47977  gricgrlic  47978  usgrexmpl12ngric  47997  usgrexmpl12ngrlic  47998  opmpoismgm  48083  neircl  48802  thincn0eu  49080  thinccic  49118  termcterm2  49146  prstchom2ALT  49168  alscn0d  49314