Theorem n0 4310

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 2195, 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 2962	. 2 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
2		neq0 4309	. 2 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
3	1, 2	bitri 278	1 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-ne 2962  df-dif 3911  df-nul 4290

This theorem is used by:  n0limd  4311  reximdva0  4313  rspn0  4314  n0rex  4315  n0moeu  4317  eqeuel  4323  ndisj  4328  pssnel  4434  r19.2z  4465  r19.3rz  4467  uniintsn  4955  iunn0  5036  trintss  5242  intex  5319  notsep  5339  reusv2lem1  5374  nnullss  5448  exss  5449  opabn0  5543  wefrc  5660  wereu2  5663  dmxp  5924  xpnz  6161  dmsnn0  6213  unixp0  6291  xpco  6297  frpomin  6348  onfr  6407  iotanul2  6516  fveqdmss  7080  eldmrexrnb  7094  isofrlem  7349  limuni3  7857  soex  7927  f1oweALT  7978  fo1stres  8021  fo2ndres  8022  ecdmn0  8756  fsetprcnex  8868  map0g  8891  ixpn0  8937  resixpfo  8943  domdifsn  9058  xpdom3  9073  fodomr  9126  mapdom3  9147  0sdom1dom  9216  unblem2  9263  fodomfir  9297  marypha1lem  9403  brwdom2  9545  unxpwdom2  9560  ixpiunwdom  9562  zfreg  9568  epfrs  9710  frmin  9731  scott0b  9876  scott0OLD  9877  scotteld  9886  cplem1  9889  cplem1OLD  9890  karden  9898  fseqen  10030  finacn  10053  iunfictbso  10117  aceq2  10122  dfac3  10124  dfac9  10139  kmlem6  10158  kmlem8  10160  infpss  10218  fin23lem7  10318  enfin2i  10323  fin23lem21  10341  fin23lem31  10345  isf32lem9  10363  isf34lem4  10379  axdc2lem  10450  axdc3lem4  10455  ac6c4  10483  ac9  10485  ac6s4  10492  ac9s  10495  ttukeyg  10519  fpwwe2lem11  10644  wun0  10721  tsk0  10766  gruina  10821  genpn0  11006  prlem934  11036  ltaddpr  11037  ltexprlem1  11039  prlem936  11050  reclem2pr  11051  suplem1pr  11055  supsr  11115  axpre-sup  11172  dedekind  11391  dedekindle  11392  negn0  11661  infm3  12192  supaddc  12200  supadd  12201  supmul1  12202  supmullem2  12204  supmul  12205  zsupss  12979  xrsupsslem  13351  xrinfmsslem  13352  supxrre  13371  infxrre  13381  ixxub  13411  ixxlb  13412  ioorebas  13496  fzn0  13584  fzon0  13725  hashgt0elexb  14458  swrdcl  14705  pfxcl  14739  maxprmfct  16793  4sqlem12  17041  vdwmc  17063  ramz  17110  ramub1  17113  mreiincl  17673  mremre  17681  mreexexlem4d  17728  iscatd2  17762  catcone0  17768  cic  17881  drsdirfi  18386  mgmpropd  18734  opifismgm  18742  dfgrp3lem  19135  dfgrp3e  19137  issubg2  19239  subgint  19248  qsxpid  19274  giclcl  19374  gicrcl  19375  gicsym  19376  gictr  19377  gicen  19379  gicsubgen  19380  cntzssv  19429  symggen  19571  psgnunilem3  19597  sylow1lem4  19702  odcau  19705  sylow3  19734  cyggex2  19998  giccyg  20001  pgpfac1lem5  20182  riclcl  20634  ricrcl  20635  ricsym  20636  rictr  20637  isbrric2  20638  subrngint  20696  subrgint  20731  abvn0b  20976  lss0cl  21105  lmiclcl  21228  lmicrcl  21229  lmicsym  21230  lspsnat  21306  lspprat  21314  lidlunin0  21398  qsidomlem2  21518  cnsubrg  21614  nzerooringczr  21667  cygzn  21757  lmiclbs  22024  lmisfree  22029  lmictra  22032  mpfrcl  22273  ply1frcl  22515  mdetdiaglem  22792  mdet0  22800  toponmre  23287  iunconnlem  23621  iunconn  23622  unconn  23623  clsconn  23624  2ndcdisj  23650  2ndcsep  23653  1stcelcls  23655  locfincmp  23720  comppfsc  23726  txcls  23798  hmphsym  23976  hmphtr  23977  hmphen  23979  haushmphlem  23981  cmphmph  23982  connhmph  23983  reghmph  23987  nrmhmph  23988  hmphdis  23990  hmphen2  23993  fbdmn0  24028  isfbas2  24029  fbssint  24032  trfbas2  24037  filtop  24049  isfil2  24050  elfg  24065  fgcl  24072  filssufilg  24105  uffix2  24118  ufildom1  24120  hauspwpwf1  24181  hausflf2  24192  alexsubALTlem2  24242  ptcmplem2  24247  cnextf  24260  tgptsmscld  24345  ustfilxp  24407  xbln0  24608  lpbl  24697  met2ndci  24716  metustfbas  24751  restmetu  24764  reconn  25023  opnreen  25026  metdsre  25048  phtpcer  25191  phtpc01  25192  phtpcco2  25195  pcohtpy  25216  cfilfcls  25470  cmetcaulem  25484  cmetcau  25485  bcthlem5  25524  ovolicc2lem2  25714  ovolicc2lem5  25717  ioorcl2  25768  ioorinv2  25771  itg11  25887  dvlip  26189  dvne0  26207  fta1g  26364  plyssc  26394  fta1  26506  vieta1lem2  26509  nobdaymin  27983  sltstr  28017  ltslpss  28138  lrrecfr  28173  oncutlt  28494  hpgerlem  29084  axcontlem4  29354  axcontlem10  29360  upgrex  29479  fusgrn0degnn0  29886  uhgrvd00  29921  wspthsnonn0vne  30303  eulerpath  30629  frgrwopreglem2  30701  ubthlem1  31259  shintcli  31718  2ndimaxp  33028  fpwrelmapffslem  33114  qsdrng  33810  1arithidom  33858  dimcl  34024  lmimdim  34025  lmicdim  34026  lvecdim0i  34027  lvecdim0  34028  lssdimle  34029  dimpropd  34030  dimkerim  34048  fedgmul  34052  extdg1id  34087  fmcncfil  34352  insiga  34559  unelldsys  34580  bnj1189  35429  bnj1279  35438  rankscott  35546  axregszf  35566  karddom  35598  kardsdom  35599  vonf1oonfo  35623  pconnconn  35744  txsconn  35754  cvmsss2  35787  cvmopnlem  35791  cvmfolem  35792  cvmliftmolem2  35795  cvmlift2lem10  35825  cvmliftpht  35831  cvmlift3lem8  35839  eldm3  36274  fundmpss  36280  elima4  36289  neibastop1  36911  neibastop2lem  36912  neibastop2  36913  fnemeet2  36919  fnejoin2  36921  neifg  36923  tailfb  36929  filnetlem3  36932  mh-infprim1bi  37098  bj-n0i  37628  bj-rest10  37771  bj-restn0  37773  poimirlem30  38342  itg2addnclem2  38364  prdsbnd2  38487  heibor1lem  38501  bfp  38516  divrngidl  38720  eldmres3  38973  rnxrn  39111  eldmxrncnvepres2  39125  trcoss2  39264  atex  40221  llnn0  40331  lplnn0N  40362  lvoln0N  40406  pmapglb2N  40586  pmapglb2xN  40587  elpaddn0  40615  osumcllem8N  40778  pexmidlem5N  40789  diaglbN  41870  diaintclN  41873  dibglbN  41981  dibintclN  41982  dihglblem2aN  42108  dihglblem5  42113  dihglbcpreN  42115  dihintcl  42159  unitscyglem5  43007  riccrng1  43330  ricdrng1  43337  rencldnfilem  43588  kelac1  43831  lnmlmic  43856  gicabl  43867  neik0pk1imk0  44814  ntrneineine0lem  44850  onfrALT  45299  onfrALTVD  45640  iunconnlem2  45684  relpfrlem  45703  dfac5prim  45740  permac8prim  45764  snelmap  45843  eliin2f  45863  disjinfi  45951  mapss2  45963  difmap  45964  infrpge  46108  infxrlesupxr  46191  inficc  46291  fsumnncl  46329  ellimciota  46371  islpcn  46394  lptre2pt  46395  stoweidlem35  46790  fourierdlem31  46893  fourier2  46982  qndenserrnbllem  47049  qndenserrnopn  47053  qndenserrn  47054  intsaluni  47084  sge0cl  47136  ovn0lem  47320  ovnsubaddlem2  47326  hoidmvval0b  47345  hspdifhsp  47371  fsetprcnexALT  47840  uniimaelsetpreimafv  48186  imasetpreimafvbijlemfv1  48193  dfgric2  48721  gricuspgr  48724  gricsym  48727  grictr  48729  gricen  48731  dfgrlic2  48814  dfgrlic3  48816  grlicen  48823  gricgrlic  48824  usgrexmpl12ngric  48844  usgrexmpl12ngrlic  48845  opmpoismgm  48973  neircl  49724  sectrcl  49841  invrcl  49843  isorcl  49852  iinfssc  49876  iinfsubc  49877  imaid  49973  thincn0eu  50250  thinccic  50290  termcterm2  50333  eufunc  50341  euendfunc  50345  diag1f1o  50353  diag2f1o  50356  prstchom2ALT  50383  rellan  50442  relran  50443  alsralrex  50631