Theorem n0 4303

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2147   ≠ wne 2959  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-ne 2960  df-dif 4050  df-nul 4282

This theorem is used by:  n0limd  4304  reximdva0  4306  rspn0  4307  n0rex  4308  n0moeu  4310  eqeuel  4316  ndisj  4321  pssnel  4427  r19.2z  4458  r19.3rz  4460  uniintsn  4948  iunn0  5028  trintss  5235  intex  5310  notsep  5330  reusv2lem1  5365  nnullss  5435  exss  5436  opabn0  5533  wefrc  5650  wereu2  5653  dmxp  5919  xpnz  6163  dmsnn0  6222  unixp0  6305  xpco  6313  frpomin  6364  onfr  6423  iotanul2  6532  fveqdmss  7105  eldmrexrnb  7119  isofrlem  7374  limuni3  7890  soex  7960  f1oweALT  8011  fo1stres  8054  fo2ndres  8055  ecdmn0  8801  fsetprcnex  8915  map0g  8943  ixpn0  8989  resixpfo  8995  domdifsn  9110  xpdom3  9125  fodomr  9178  mapdom3  9199  0sdom1dom  9268  unblem2  9316  fodomfir  9350  marypha1lem  9455  brwdom2  9597  unxpwdom2  9612  ixpiunwdom  9614  zfreg  9620  epfrs  9762  frmin  9783  scott0b  9967  scott0OLD  9968  scotteld  9977  cplem1  9980  cplem1OLD  9981  karden  9989  fseqen  10136  finacn  10159  iunfictbso  10223  aceq2  10228  dfac3  10230  dfac9  10245  kmlem6  10264  kmlem8  10266  infpss  10324  fin23lem7  10424  enfin2i  10429  fin23lem21  10447  fin23lem31  10451  isf32lem9  10469  isf34lem4  10485  axdc2lem  10556  axdc3lem4  10561  ac6c4  10589  ac9  10591  ac6s4  10598  ac9s  10601  ttukeyg  10625  fpwwe2lem11  10756  wun0  10833  tsk0  10878  gruina  10933  genpn0  11118  prlem934  11148  ltaddpr  11149  ltexprlem1  11151  prlem936  11162  reclem2pr  11163  suplem1pr  11167  supsr  11227  axpre-sup  11284  dedekind  11503  dedekindle  11504  negn0  11775  infm3  12306  supaddc  12314  supadd  12315  supmul1  12316  supmullem2  12318  supmul  12319  zsupss  13094  xrsupsslem  13467  xrinfmsslem  13468  supxrre  13487  infxrre  13497  ixxub  13527  ixxlb  13528  ioorebas  13612  fzn0  13701  fzon0  13842  hashgt0elexb  14576  swrdcl  14824  pfxcl  14858  maxprmfct  16917  4sqlem12  17166  vdwmc  17188  ramz  17235  ramub1  17238  mreiincl  17798  mremre  17806  mreexexlem4d  17853  iscatd2  17887  catcone0  17893  cic  18006  drsdirfi  18511  mgmpropd  18861  opifismgm  18869  dfgrp3lem  19280  dfgrp3e  19282  issubg2  19384  subgint  19393  qsxpid  19419  giclcl  19520  gicrcl  19521  gicsym  19522  gictr  19523  gicen  19525  gicsubgen  19526  cntzssv  19575  symggen  19717  psgnunilem3  19743  sylow1lem4  19848  odcau  19851  sylow3  19880  cyggex2  20144  giccyg  20147  pgpfac1lem5  20328  riclcl  20782  ricrcl  20783  ricsym  20784  rictr  20785  isbrric2  20786  subrngint  20845  subrgint  20880  abvn0b  21126  lss0cl  21255  lmiclcl  21378  lmicrcl  21379  lmicsym  21380  lspsnat  21456  lspprat  21464  lidlunin0  21548  qsidomlem2  21670  cnsubrg  21766  nzerooringczr  21819  cygzn  21909  lmiclbs  22176  lmisfree  22181  lmictra  22184  mpfrcl  22427  ply1frcl  22669  mdetdiaglem  22946  mdet0  22954  toponmre  23444  iunconnlem  23778  iunconn  23779  unconn  23780  clsconn  23781  2ndcdisj  23808  2ndcsep  23811  1stcelcls  23813  locfincmp  23878  comppfsc  23884  txcls  23956  hmphsym  24134  hmphtr  24135  hmphen  24137  haushmphlem  24139  cmphmph  24140  connhmph  24141  reghmph  24145  nrmhmph  24146  hmphdis  24148  hmphen2  24151  fbdmn0  24186  isfbas2  24187  fbssint  24190  trfbas2  24195  filtop  24207  isfil2  24208  elfg  24223  fgcl  24230  filssufilg  24263  uffix2  24276  ufildom1  24278  hauspwpwf1  24339  hausflf2  24350  alexsubALTlem2  24400  ptcmplem2  24405  cnextf  24418  tgptsmscld  24503  ustfilxp  24565  xbln0  24766  lpbl  24855  met2ndci  24874  metustfbas  24909  restmetu  24922  reconn  25181  opnreen  25184  metdsre  25206  phtpcer  25349  phtpc01  25350  phtpcco2  25353  pcohtpy  25374  cfilfcls  25628  cmetcaulem  25642  cmetcau  25643  bcthlem5  25682  ovolicc2lem2  25872  ovolicc2lem5  25875  ioorcl2  25926  ioorinv2  25929  itg11  26045  dvlip  26346  dvne0  26364  fta1g  26521  plyssc  26551  fta1  26662  vieta1lem2  26667  nobdaymin  28172  sltstr  28206  ltslpss  28327  lrrecfr  28362  oncutlt  28683  hpgerlem  29276  axcontlem4  29578  axcontlem10  29584  upgrex  29703  fusgrn0degnn0  30113  uhgrvd00  30148  wspthsnonn0vne  30539  eulerpath  30875  frgrwopreglem2  30947  ubthlem1  31505  shintcli  31964  2ndimaxp  33315  fpwrelmapffslem  33397  qsdrng  34105  1arithidom  34153  dimcl  34318  lmimdim  34319  lmicdim  34320  lvecdim0i  34321  lvecdim0  34322  lssdimle  34323  dimpropd  34324  dimkerim  34342  fedgmul  34346  extdg1id  34381  fmcncfil  34646  insiga  34853  unelldsys  34874  bnj1189  35722  bnj1279  35731  soinfdom  35813  rankscott  35851  axregszf  35910  karddom  35942  kardsdom  35943  vonf1oonfo  36062  pconnconn  36176  txsconn  36186  cvmsss2  36219  cvmopnlem  36223  cvmfolem  36224  cvmliftmolem2  36227  cvmlift2lem10  36257  cvmliftpht  36263  cvmlift3lem8  36271  eldm3  36717  fundmpss  36723  elima4  36731  neibastop1  37338  neibastop2lem  37339  neibastop2  37340  fnemeet2  37346  fnejoin2  37348  neifg  37350  tailfb  37356  filnetlem3  37359  mh-infprim1bi  37525  bj-n0i  38055  bj-rest10  38213  bj-restn0  38215  poimirlem30  38773  itg2addnclem2  38795  prdsbnd2  38932  heibor1lem  38946  bfp  38961  divrngidl  39165  eldmres3  39418  rnxrn  39556  eldmxrncnvepres2  39570  trcoss2  39709  atex  40666  llnn0  40776  lplnn0N  40807  lvoln0N  40851  pmapglb2N  41031  pmapglb2xN  41032  elpaddn0  41060  osumcllem8N  41223  pexmidlem5N  41234  diaglbN  42315  diaintclN  42318  dibglbN  42426  dibintclN  42427  dihglblem2aN  42553  dihglblem5  42558  dihglbcpreN  42560  dihintcl  42604  unitscyglem5  43452  riccrng1  43786  ricdrng1  43796  rencldnfilem  44031  kelac1  44269  lnmlmic  44294  gicabl  44305  neik0pk1imk0  45250  ntrneineine0lem  45286  onfrALT  45734  onfrALTVD  46075  iunconnlem2  46119  relpfrlem  46149  dfac5prim  46186  permac8prim  46210  snelmap  46314  eliin2f  46334  disjinfi  46422  mapss2  46434  difmap  46435  infrpge  46578  infxrlesupxr  46661  inficc  46761  fsumnncl  46799  ellimciota  46841  islpcn  46864  lptre2pt  46865  stoweidlem35  47260  fourierdlem31  47363  fourier2  47452  qndenserrnbllem  47519  qndenserrnopn  47523  qndenserrn  47524  intsaluni  47554  sge0cl  47606  ovn0lem  47790  ovnsubaddlem2  47796  hoidmvval0b  47815  hspdifhsp  47841  fsetprcnexALT  48347  uniimaelsetpreimafv  48693  imasetpreimafvbijlemfv1  48700  dfgric2  49228  gricuspgr  49231  gricsym  49234  grictr  49236  gricen  49238  dfgrlic2  49321  dfgrlic3  49323  grlicen  49330  gricgrlic  49331  usgrexmpl12ngric  49351  usgrexmpl12ngrlic  49352  opmpoismgm  49479  neircl  50234  sectrcl  50351  invrcl  50353  isorcl  50362  iinfssc  50386  iinfsubc  50387  imaid  50485  thincn0eu  50781  thinccic  50821  termcterm2  50864  eufunc  50872  euendfunc  50876  diag1f1o  50884  diag2f1o  50890  prstchom2ALT  50917  rellan  51021  relran  51022  alsralrex  51220