Theorem n0 4358

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1536  ∃wex 1775   ∈ wcel 2105   ≠ wne 2937  ∅c0 4338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-ne 2938  df-dif 3965  df-nul 4339

This theorem is referenced by:  reximdva0  4360  rspn0  4361  n0rex  4362  n0moeu  4364  eqeuel  4370  ndisj  4375  pssnel  4476  r19.2z  4500  r19.2zb  4501  r19.3rz  4502  uniintsn  4989  iunn0  5071  trintss  5283  intex  5349  notzfaus  5368  reusv2lem1  5403  nnullss  5472  exss  5473  opabn0  5562  wefrc  5682  wereu2  5685  dmxp  5941  dmxpOLD  5942  xpnz  6180  dmsnn0  6228  unixp0  6304  xpco  6310  frpomin  6362  onfr  6424  iotanul2  6532  fveqdmss  7097  eldmrexrnb  7111  isofrlem  7359  limuni3  7872  soex  7943  f1oweALT  7995  fo1stres  8038  fo2ndres  8039  ecdmn0  8792  fsetprcnex  8900  map0g  8922  ixpn0  8968  resixpfo  8974  domdifsn  9092  xpdom3  9108  fodomr  9166  mapdom3  9187  0sdom1dom  9271  unblem2  9326  fodomfir  9365  marypha1lem  9470  brwdom2  9610  unxpwdom2  9625  ixpiunwdom  9627  zfreg  9632  epfrs  9768  frmin  9786  scott0  9923  cplem1  9926  fseqen  10064  finacn  10087  iunfictbso  10151  aceq2  10156  dfac3  10158  dfac9  10174  kmlem6  10193  kmlem8  10195  infpss  10253  fin23lem7  10353  enfin2i  10358  fin23lem21  10376  fin23lem31  10380  isf32lem9  10398  isf34lem4  10414  axdc2lem  10485  axdc3lem4  10490  ac6c4  10518  ac9  10520  ac6s4  10527  ac9s  10530  ttukeyg  10554  fpwwe2lem11  10678  wun0  10755  tsk0  10800  gruina  10855  genpn0  11040  prlem934  11070  ltaddpr  11071  ltexprlem1  11073  prlem936  11084  reclem2pr  11085  suplem1pr  11089  supsr  11149  axpre-sup  11206  dedekind  11421  dedekindle  11422  negn0  11689  infm3  12224  supaddc  12232  supadd  12233  supmul1  12234  supmullem2  12236  supmul  12237  zsupss  12976  xrsupsslem  13345  xrinfmsslem  13346  supxrre  13365  infxrre  13374  ixxub  13404  ixxlb  13405  ioorebas  13487  fzn0  13574  fzon0  13713  hashgt0elexb  14437  swrdcl  14679  pfxcl  14711  maxprmfct  16742  4sqlem12  16989  vdwmc  17011  ramz  17058  ramub1  17061  mreiincl  17640  mremre  17648  mreexexlem4d  17691  iscatd2  17725  catcone0  17731  cic  17846  drsdirfi  18362  mgmpropd  18676  opifismgm  18684  dfgrp3lem  19068  dfgrp3e  19070  issubg2  19171  subgint  19180  giclcl  19303  gicrcl  19304  gicsym  19305  gictr  19306  gicen  19308  gicsubgen  19309  cntzssv  19358  symggen  19502  psgnunilem3  19528  sylow1lem4  19633  odcau  19636  sylow3  19665  cyggex2  19929  giccyg  19932  pgpfac1lem5  20113  brric2  20522  subrngint  20576  subrgint  20611  abvn0b  20853  lss0cl  20962  lmiclcl  21086  lmicrcl  21087  lmicsym  21088  lspsnat  21164  lspprat  21172  cnsubrg  21462  nzerooringczr  21508  cygzn  21606  lmiclbs  21874  lmisfree  21879  lmictra  21882  mpfrcl  22126  ply1frcl  22337  mdetdiaglem  22619  mdet0  22627  toponmre  23116  iunconnlem  23450  iunconn  23451  unconn  23452  clsconn  23453  2ndcdisj  23479  2ndcsep  23482  1stcelcls  23484  locfincmp  23549  comppfsc  23555  txcls  23627  hmphsym  23805  hmphtr  23806  hmphen  23808  haushmphlem  23810  cmphmph  23811  connhmph  23812  reghmph  23816  nrmhmph  23817  hmphdis  23819  hmphen2  23822  fbdmn0  23857  isfbas2  23858  fbssint  23861  trfbas2  23866  filtop  23878  isfil2  23879  elfg  23894  fgcl  23901  filssufilg  23934  uffix2  23947  ufildom1  23949  hauspwpwf1  24010  hausflf2  24021  alexsubALTlem2  24071  ptcmplem2  24076  cnextf  24089  tgptsmscld  24174  ustfilxp  24236  xbln0  24439  lpbl  24531  met2ndci  24550  metustfbas  24585  restmetu  24598  reconn  24863  opnreen  24866  metdsre  24888  phtpcer  25040  phtpc01  25041  phtpcco2  25045  pcohtpy  25066  cfilfcls  25321  cmetcaulem  25335  cmetcau  25336  bcthlem5  25375  ovolicc2lem2  25566  ovolicc2lem5  25569  ioorcl2  25620  ioorinv2  25623  itg11  25739  dvlip  26046  dvne0  26064  fta1g  26223  plyssc  26253  fta1  26364  vieta1lem2  26367  nocvxmin  27837  sslttr  27866  sltlpss  27959  lrrecfr  27990  hpgerlem  28787  axcontlem4  28996  axcontlem10  29002  upgrex  29123  fusgrn0degnn0  29531  uhgrvd00  29566  wspthsnonn0vne  29946  eulerpath  30269  frgrwopreglem2  30341  ubthlem1  30898  shintcli  31357  n0limd  32500  2ndimaxp  32662  fpwrelmapffslem  32749  qsxpid  33369  qsidomlem2  33460  qsdrng  33504  1arithidom  33544  dimcl  33629  lmimdim  33630  lmicdim  33631  lvecdim0i  33632  lvecdim0  33633  lssdimle  33634  dimpropd  33635  dimkerim  33654  fedgmul  33658  extdg1id  33690  fmcncfil  33891  insiga  34117  unelldsys  34138  bnj1189  35001  bnj1279  35010  pconnconn  35215  txsconn  35225  cvmsss2  35258  cvmopnlem  35262  cvmfolem  35263  cvmliftmolem2  35266  cvmlift2lem10  35296  cvmliftpht  35302  cvmlift3lem8  35310  eldm3  35740  fundmpss  35747  elima4  35756  neibastop1  36341  neibastop2lem  36342  neibastop2  36343  fnemeet2  36349  fnejoin2  36351  neifg  36353  tailfb  36359  filnetlem3  36362  bj-n0i  36933  bj-rest10  37070  bj-restn0  37072  poimirlem30  37636  itg2addnclem2  37658  prdsbnd2  37781  heibor1lem  37795  bfp  37810  divrngidl  38014  rnxrn  38379  trcoss2  38465  atex  39388  llnn0  39498  lplnn0N  39529  lvoln0N  39573  pmapglb2N  39753  pmapglb2xN  39754  elpaddn0  39782  osumcllem8N  39945  pexmidlem5N  39956  diaglbN  41037  diaintclN  41040  dibglbN  41148  dibintclN  41149  dihglblem2aN  41275  dihglblem5  41280  dihglbcpreN  41282  dihintcl  41326  unitscyglem5  42180  ricsym  42505  rictr  42506  riccrng1  42507  ricdrng1  42514  rencldnfilem  42807  kelac1  43051  lnmlmic  43076  gicabl  43087  neik0pk1imk0  44036  ntrneineine0lem  44072  scotteld  44241  onfrALT  44546  onfrALTVD  44888  iunconnlem2  44932  snelmap  45021  eliin2f  45043  disjinfi  45134  mapss2  45147  difmap  45149  infrpge  45300  infxrlesupxr  45385  inficc  45486  fsumnncl  45527  ellimciota  45569  islpcn  45594  lptre2pt  45595  stoweidlem35  45990  fourierdlem31  46093  fourier2  46182  qndenserrnbllem  46249  qndenserrnopn  46253  qndenserrn  46254  intsaluni  46284  sge0cl  46336  ovn0lem  46520  ovnsubaddlem2  46526  hoidmvval0b  46545  hspdifhsp  46571  fsetprcnexALT  47011  uniimaelsetpreimafv  47320  imasetpreimafvbijlemfv1  47327  dfgric2  47821  gricuspgr  47824  gricsym  47827  grictr  47829  gricen  47831  dfgrlic2  47903  dfgrlic3  47905  grlicen  47912  gricgrlic  47913  usgrexmpl12ngric  47932  usgrexmpl12ngrlic  47933  opmpoismgm  48010  neircl  48700  thincn0eu  48831  thinccic  48861  prstchom2ALT  48879  alscn0d  49025