Theorem n0 4319

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2926  ∅c0 4299

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 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-ne 2927  df-dif 3920  df-nul 4300

This theorem is referenced by:  reximdva0  4321  rspn0  4322  n0rex  4323  n0moeu  4325  eqeuel  4331  ndisj  4336  pssnel  4437  r19.2z  4461  r19.2zb  4462  r19.3rz  4463  uniintsn  4952  iunn0  5034  trintss  5236  intex  5302  notzfaus  5321  reusv2lem1  5356  nnullss  5425  exss  5426  opabn0  5516  wefrc  5635  wereu2  5638  dmxp  5895  dmxpOLD  5896  xpnz  6135  dmsnn0  6183  unixp0  6259  xpco  6265  frpomin  6316  onfr  6374  iotanul2  6484  fveqdmss  7053  eldmrexrnb  7067  isofrlem  7318  limuni3  7831  soex  7900  f1oweALT  7954  fo1stres  7997  fo2ndres  7998  ecdmn0  8726  fsetprcnex  8838  map0g  8860  ixpn0  8906  resixpfo  8912  domdifsn  9028  xpdom3  9044  fodomr  9098  mapdom3  9119  0sdom1dom  9192  unblem2  9247  fodomfir  9286  marypha1lem  9391  brwdom2  9533  unxpwdom2  9548  ixpiunwdom  9550  zfreg  9555  epfrs  9691  frmin  9709  scott0  9846  cplem1  9849  fseqen  9987  finacn  10010  iunfictbso  10074  aceq2  10079  dfac3  10081  dfac9  10097  kmlem6  10116  kmlem8  10118  infpss  10176  fin23lem7  10276  enfin2i  10281  fin23lem21  10299  fin23lem31  10303  isf32lem9  10321  isf34lem4  10337  axdc2lem  10408  axdc3lem4  10413  ac6c4  10441  ac9  10443  ac6s4  10450  ac9s  10453  ttukeyg  10477  fpwwe2lem11  10601  wun0  10678  tsk0  10723  gruina  10778  genpn0  10963  prlem934  10993  ltaddpr  10994  ltexprlem1  10996  prlem936  11007  reclem2pr  11008  suplem1pr  11012  supsr  11072  axpre-sup  11129  dedekind  11344  dedekindle  11345  negn0  11614  infm3  12149  supaddc  12157  supadd  12158  supmul1  12159  supmullem2  12161  supmul  12162  zsupss  12903  xrsupsslem  13274  xrinfmsslem  13275  supxrre  13294  infxrre  13304  ixxub  13334  ixxlb  13335  ioorebas  13419  fzn0  13506  fzon0  13645  hashgt0elexb  14374  swrdcl  14617  pfxcl  14649  maxprmfct  16686  4sqlem12  16934  vdwmc  16956  ramz  17003  ramub1  17006  mreiincl  17564  mremre  17572  mreexexlem4d  17615  iscatd2  17649  catcone0  17655  cic  17768  drsdirfi  18273  mgmpropd  18585  opifismgm  18593  dfgrp3lem  18977  dfgrp3e  18979  issubg2  19080  subgint  19089  giclcl  19212  gicrcl  19213  gicsym  19214  gictr  19215  gicen  19217  gicsubgen  19218  cntzssv  19267  symggen  19407  psgnunilem3  19433  sylow1lem4  19538  odcau  19541  sylow3  19570  cyggex2  19834  giccyg  19837  pgpfac1lem5  20018  brric2  20422  subrngint  20476  subrgint  20511  abvn0b  20752  lss0cl  20860  lmiclcl  20984  lmicrcl  20985  lmicsym  20986  lspsnat  21062  lspprat  21070  cnsubrg  21351  nzerooringczr  21397  cygzn  21487  lmiclbs  21753  lmisfree  21758  lmictra  21761  mpfrcl  21999  ply1frcl  22212  mdetdiaglem  22492  mdet0  22500  toponmre  22987  iunconnlem  23321  iunconn  23322  unconn  23323  clsconn  23324  2ndcdisj  23350  2ndcsep  23353  1stcelcls  23355  locfincmp  23420  comppfsc  23426  txcls  23498  hmphsym  23676  hmphtr  23677  hmphen  23679  haushmphlem  23681  cmphmph  23682  connhmph  23683  reghmph  23687  nrmhmph  23688  hmphdis  23690  hmphen2  23693  fbdmn0  23728  isfbas2  23729  fbssint  23732  trfbas2  23737  filtop  23749  isfil2  23750  elfg  23765  fgcl  23772  filssufilg  23805  uffix2  23818  ufildom1  23820  hauspwpwf1  23881  hausflf2  23892  alexsubALTlem2  23942  ptcmplem2  23947  cnextf  23960  tgptsmscld  24045  ustfilxp  24107  xbln0  24309  lpbl  24398  met2ndci  24417  metustfbas  24452  restmetu  24465  reconn  24724  opnreen  24727  metdsre  24749  phtpcer  24901  phtpc01  24902  phtpcco2  24906  pcohtpy  24927  cfilfcls  25181  cmetcaulem  25195  cmetcau  25196  bcthlem5  25235  ovolicc2lem2  25426  ovolicc2lem5  25429  ioorcl2  25480  ioorinv2  25483  itg11  25599  dvlip  25905  dvne0  25923  fta1g  26082  plyssc  26112  fta1  26223  vieta1lem2  26226  nocvxmin  27697  sslttr  27726  sltlpss  27826  lrrecfr  27857  onscutlt  28172  hpgerlem  28699  axcontlem4  28901  axcontlem10  28907  upgrex  29026  fusgrn0degnn0  29434  uhgrvd00  29469  wspthsnonn0vne  29854  eulerpath  30177  frgrwopreglem2  30249  ubthlem1  30806  shintcli  31265  n0limd  32408  2ndimaxp  32577  fpwrelmapffslem  32662  qsxpid  33340  qsidomlem2  33431  qsdrng  33475  1arithidom  33515  dimcl  33605  lmimdim  33606  lmicdim  33607  lvecdim0i  33608  lvecdim0  33609  lssdimle  33610  dimpropd  33611  dimkerim  33630  fedgmul  33634  extdg1id  33668  fmcncfil  33928  insiga  34134  unelldsys  34155  bnj1189  35006  bnj1279  35015  pconnconn  35225  txsconn  35235  cvmsss2  35268  cvmopnlem  35272  cvmfolem  35273  cvmliftmolem2  35276  cvmlift2lem10  35306  cvmliftpht  35312  cvmlift3lem8  35320  eldm3  35755  fundmpss  35761  elima4  35770  neibastop1  36354  neibastop2lem  36355  neibastop2  36356  fnemeet2  36362  fnejoin2  36364  neifg  36366  tailfb  36372  filnetlem3  36375  bj-n0i  36946  bj-rest10  37083  bj-restn0  37085  poimirlem30  37651  itg2addnclem2  37673  prdsbnd2  37796  heibor1lem  37810  bfp  37825  divrngidl  38029  eldmres3  38272  rnxrn  38391  eldmxrncnvepres2  38404  trcoss2  38482  atex  39407  llnn0  39517  lplnn0N  39548  lvoln0N  39592  pmapglb2N  39772  pmapglb2xN  39773  elpaddn0  39801  osumcllem8N  39964  pexmidlem5N  39975  diaglbN  41056  diaintclN  41059  dibglbN  41167  dibintclN  41168  dihglblem2aN  41294  dihglblem5  41299  dihglbcpreN  41301  dihintcl  41345  unitscyglem5  42194  ricsym  42514  rictr  42515  riccrng1  42516  ricdrng1  42523  rencldnfilem  42815  kelac1  43059  lnmlmic  43084  gicabl  43095  neik0pk1imk0  44043  ntrneineine0lem  44079  scotteld  44242  onfrALT  44546  onfrALTVD  44887  iunconnlem2  44931  relpfrlem  44950  dfac5prim  44987  permac8prim  45011  snelmap  45083  eliin2f  45105  disjinfi  45193  mapss2  45206  difmap  45208  infrpge  45354  infxrlesupxr  45439  inficc  45539  fsumnncl  45577  ellimciota  45619  islpcn  45644  lptre2pt  45645  stoweidlem35  46040  fourierdlem31  46143  fourier2  46232  qndenserrnbllem  46299  qndenserrnopn  46303  qndenserrn  46304  intsaluni  46334  sge0cl  46386  ovn0lem  46570  ovnsubaddlem2  46576  hoidmvval0b  46595  hspdifhsp  46621  fsetprcnexALT  47067  uniimaelsetpreimafv  47401  imasetpreimafvbijlemfv1  47408  dfgric2  47919  gricuspgr  47922  gricsym  47925  grictr  47927  gricen  47929  dfgrlic2  48004  dfgrlic3  48006  grlicen  48013  gricgrlic  48014  usgrexmpl12ngric  48033  usgrexmpl12ngrlic  48034  opmpoismgm  48159  neircl  48897  sectrcl  49015  invrcl  49017  isorcl  49026  iinfssc  49050  iinfsubc  49051  imaid  49147  thincn0eu  49424  thinccic  49464  termcterm2  49507  eufunc  49515  euendfunc  49519  diag1f1o  49527  diag2f1o  49530  prstchom2ALT  49557  rellan  49616  relran  49617  alscn0d  49788