Theorem n0 4347

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 2155, ax-12 2172. (Revised by Gino Giotto, 28-Jun-2024.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1542  ∃wex 1782   ∈ wcel 2107   ≠ wne 2941  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-ne 2942  df-dif 3952  df-nul 4324

This theorem is referenced by:  reximdva0  4352  rspn0  4353  rspn0OLD  4354  n0rex  4355  n0moeu  4357  eqeuel  4363  ndisj  4368  pssnel  4471  r19.2z  4495  r19.2zb  4496  r19.3rz  4497  uniintsn  4992  iunn0  5071  trintss  5285  intex  5338  notzfaus  5362  reusv2lem1  5397  nnullss  5463  exss  5464  opabn0  5554  wefrc  5671  wereu2  5674  dmxp  5929  xpnz  6159  dmsnn0  6207  unixp0  6283  xpco  6289  frpomin  6342  onfr  6404  iotanul2  6514  fveqdmss  7081  eldmrexrnb  7094  isofrlem  7337  limuni3  7841  soex  7912  f1oweALT  7959  fo1stres  8001  fo2ndres  8002  ecdmn0  8750  fsetprcnex  8856  map0g  8878  ixpn0  8924  resixpfo  8930  domdifsn  9054  xpdom3  9070  fodomr  9128  mapdom3  9149  0sdom1dom  9238  findcard2OLD  9284  unblem2  9296  marypha1lem  9428  brwdom2  9568  unxpwdom2  9583  ixpiunwdom  9585  zfreg  9590  epfrs  9726  frmin  9744  scott0  9881  cplem1  9884  fseqen  10022  finacn  10045  iunfictbso  10109  aceq2  10114  dfac3  10116  dfac9  10131  kmlem6  10150  kmlem8  10152  infpss  10212  fin23lem7  10311  enfin2i  10316  fin23lem21  10334  fin23lem31  10338  isf32lem9  10356  isf34lem4  10372  axdc2lem  10443  axdc3lem4  10448  ac6c4  10476  ac9  10478  ac6s4  10485  ac9s  10488  ttukeyg  10512  fpwwe2lem11  10636  wun0  10713  tsk0  10758  gruina  10813  genpn0  10998  prlem934  11028  ltaddpr  11029  ltexprlem1  11031  prlem936  11042  reclem2pr  11043  suplem1pr  11047  supsr  11107  axpre-sup  11164  dedekind  11377  dedekindle  11378  negn0  11643  infm3  12173  supaddc  12181  supadd  12182  supmul1  12183  supmullem2  12185  supmul  12186  zsupss  12921  xrsupsslem  13286  xrinfmsslem  13287  supxrre  13306  infxrre  13315  ixxub  13345  ixxlb  13346  ioorebas  13428  fzn0  13515  fzon0  13650  hashgt0elexb  14362  swrdcl  14595  pfxcl  14627  maxprmfct  16646  4sqlem12  16889  vdwmc  16911  ramz  16958  ramub1  16961  mreiincl  17540  mremre  17548  mreexexlem4d  17591  iscatd2  17625  catcone0  17631  cic  17746  drsdirfi  18258  opifismgm  18578  dfgrp3lem  18921  dfgrp3e  18923  issubg2  19021  subgint  19030  giclcl  19146  gicrcl  19147  gicsym  19148  gictr  19149  gicen  19151  gicsubgen  19152  cntzssv  19192  symggen  19338  psgnunilem3  19364  sylow1lem4  19469  odcau  19472  sylow3  19501  cyggex2  19765  giccyg  19768  pgpfac1lem5  19949  brric2  20285  subrgint  20342  lss0cl  20557  lmiclcl  20681  lmicrcl  20682  lmicsym  20683  lspsnat  20758  lspprat  20766  abvn0b  20920  cnsubrg  21005  cygzn  21126  lmiclbs  21392  lmisfree  21397  lmictra  21400  mpfrcl  21648  ply1frcl  21837  mdetdiaglem  22100  mdet0  22108  toponmre  22597  iunconnlem  22931  iunconn  22932  unconn  22933  clsconn  22934  2ndcdisj  22960  2ndcsep  22963  1stcelcls  22965  locfincmp  23030  comppfsc  23036  txcls  23108  hmphsym  23286  hmphtr  23287  hmphen  23289  haushmphlem  23291  cmphmph  23292  connhmph  23293  reghmph  23297  nrmhmph  23298  hmphdis  23300  hmphen2  23303  fbdmn0  23338  isfbas2  23339  fbssint  23342  trfbas2  23347  filtop  23359  isfil2  23360  elfg  23375  fgcl  23382  filssufilg  23415  uffix2  23428  ufildom1  23430  hauspwpwf1  23491  hausflf2  23502  alexsubALTlem2  23552  ptcmplem2  23557  cnextf  23570  tgptsmscld  23655  ustfilxp  23717  xbln0  23920  lpbl  24012  met2ndci  24031  metustfbas  24066  restmetu  24079  reconn  24344  opnreen  24347  metdsre  24369  phtpcer  24511  phtpc01  24512  phtpcco2  24515  pcohtpy  24536  cfilfcls  24791  cmetcaulem  24805  cmetcau  24806  bcthlem5  24845  ovolicc2lem2  25035  ovolicc2lem5  25038  ioorcl2  25089  ioorinv2  25092  itg11  25208  dvlip  25510  dvne0  25528  fta1g  25685  plyssc  25714  fta1  25821  vieta1lem2  25824  nocvxmin  27280  sslttr  27308  sltlpss  27401  lrrecfr  27427  hpgerlem  28016  axcontlem4  28225  axcontlem10  28231  upgrex  28352  fusgrn0degnn0  28756  uhgrvd00  28791  wspthsnonn0vne  29171  eulerpath  29494  frgrwopreglem2  29566  ubthlem1  30123  shintcli  30582  2ndimaxp  31872  fpwrelmapffslem  31957  qsxpid  32474  qsidomlem2  32572  qsdrng  32611  dimcl  32688  lmimdim  32689  lvecdim0i  32690  lvecdim0  32691  lssdimle  32692  dimpropd  32693  dimkerim  32712  fedgmul  32716  extdg1id  32742  fmcncfil  32911  insiga  33135  unelldsys  33156  bnj1189  34020  bnj1279  34029  pconnconn  34222  txsconn  34232  cvmsss2  34265  cvmopnlem  34269  cvmfolem  34270  cvmliftmolem2  34273  cvmlift2lem10  34303  cvmliftpht  34309  cvmlift3lem8  34317  eldm3  34731  fundmpss  34738  elima4  34747  neibastop1  35244  neibastop2lem  35245  neibastop2  35246  fnemeet2  35252  fnejoin2  35254  neifg  35256  tailfb  35262  filnetlem3  35265  bj-n0i  35832  bj-rest10  35969  bj-restn0  35971  poimirlem30  36518  itg2addnclem2  36540  prdsbnd2  36663  heibor1lem  36677  bfp  36692  divrngidl  36896  rnxrn  37268  trcoss2  37354  atex  38277  llnn0  38387  lplnn0N  38418  lvoln0N  38462  pmapglb2N  38642  pmapglb2xN  38643  elpaddn0  38671  osumcllem8N  38834  pexmidlem5N  38845  diaglbN  39926  diaintclN  39929  dibglbN  40037  dibintclN  40038  dihglblem2aN  40164  dihglblem5  40169  dihglbcpreN  40171  dihintcl  40215  ricsym  41094  rictr  41095  riccrng1  41096  ricdrng1  41102  rencldnfilem  41558  kelac1  41805  lnmlmic  41830  gicabl  41841  neik0pk1imk0  42798  ntrneineine0lem  42834  scotteld  43005  onfrALT  43310  onfrALTVD  43652  iunconnlem2  43696  snelmap  43771  eliin2f  43793  disjinfi  43891  mapss2  43904  difmap  43906  infrpge  44061  infxrlesupxr  44146  inficc  44247  fsumnncl  44288  ellimciota  44330  islpcn  44355  lptre2pt  44356  stoweidlem35  44751  fourierdlem31  44854  fourier2  44943  qndenserrnbllem  45010  qndenserrnopn  45014  qndenserrn  45015  intsaluni  45045  sge0cl  45097  ovn0lem  45281  ovnsubaddlem2  45287  hoidmvval0b  45306  hspdifhsp  45332  fsetprcnexALT  45772  uniimaelsetpreimafv  46064  imasetpreimafvbijlemfv1  46071  mgmpropd  46545  opmpoismgm  46577  subrngint  46739  nzerooringczr  46970  neircl  47537  thincn0eu  47652  thinccic  47681  prstchom2ALT  47699  alscn0d  47842