Theorem n0 4293

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem n0

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2932  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-ne 2933  df-dif 3892  df-nul 4274

This theorem is referenced by:  reximdva0  4295  rspn0  4296  n0rex  4297  n0moeu  4299  eqeuel  4305  ndisj  4310  pssnel  4411  r19.2z  4439  r19.3rz  4441  uniintsn  4927  iunn0  5009  trintss  5211  intex  5285  notzfaus  5305  reusv2lem1  5340  nnullss  5414  exss  5415  opabn0  5508  wefrc  5625  wereu2  5628  dmxp  5884  xpnz  6123  dmsnn0  6171  unixp0  6247  xpco  6253  frpomin  6304  onfr  6362  iotanul2  6471  fveqdmss  7030  eldmrexrnb  7044  isofrlem  7295  limuni3  7803  soex  7872  f1oweALT  7925  fo1stres  7968  fo2ndres  7969  ecdmn0  8696  fsetprcnex  8809  map0g  8832  ixpn0  8878  resixpfo  8884  domdifsn  8998  xpdom3  9013  fodomr  9066  mapdom3  9087  0sdom1dom  9156  unblem2  9203  fodomfir  9238  marypha1lem  9346  brwdom2  9488  unxpwdom2  9503  ixpiunwdom  9505  zfreg  9511  epfrs  9652  frmin  9673  scott0  9810  cplem1  9813  fseqen  9949  finacn  9972  iunfictbso  10036  aceq2  10041  dfac3  10043  dfac9  10059  kmlem6  10078  kmlem8  10080  infpss  10138  fin23lem7  10238  enfin2i  10243  fin23lem21  10261  fin23lem31  10265  isf32lem9  10283  isf34lem4  10299  axdc2lem  10370  axdc3lem4  10375  ac6c4  10403  ac9  10405  ac6s4  10412  ac9s  10415  ttukeyg  10439  fpwwe2lem11  10564  wun0  10641  tsk0  10686  gruina  10741  genpn0  10926  prlem934  10956  ltaddpr  10957  ltexprlem1  10959  prlem936  10970  reclem2pr  10971  suplem1pr  10975  supsr  11035  axpre-sup  11092  dedekind  11309  dedekindle  11310  negn0  11579  infm3  12115  supaddc  12123  supadd  12124  supmul1  12125  supmullem2  12127  supmul  12128  zsupss  12887  xrsupsslem  13259  xrinfmsslem  13260  supxrre  13279  infxrre  13289  ixxub  13319  ixxlb  13320  ioorebas  13404  fzn0  13492  fzon0  13632  hashgt0elexb  14364  swrdcl  14608  pfxcl  14640  maxprmfct  16679  4sqlem12  16927  vdwmc  16949  ramz  16996  ramub1  16999  mreiincl  17558  mremre  17566  mreexexlem4d  17613  iscatd2  17647  catcone0  17653  cic  17766  drsdirfi  18271  mgmpropd  18619  opifismgm  18627  dfgrp3lem  19014  dfgrp3e  19016  issubg2  19117  subgint  19126  giclcl  19248  gicrcl  19249  gicsym  19250  gictr  19251  gicen  19253  gicsubgen  19254  cntzssv  19303  symggen  19445  psgnunilem3  19471  sylow1lem4  19576  odcau  19579  sylow3  19608  cyggex2  19872  giccyg  19875  pgpfac1lem5  20056  brric2  20483  subrngint  20537  subrgint  20572  abvn0b  20813  lss0cl  20942  lmiclcl  21065  lmicrcl  21066  lmicsym  21067  lspsnat  21143  lspprat  21151  cnsubrg  21407  nzerooringczr  21460  cygzn  21550  lmiclbs  21817  lmisfree  21822  lmictra  21825  mpfrcl  22063  ply1frcl  22283  mdetdiaglem  22563  mdet0  22571  toponmre  23058  iunconnlem  23392  iunconn  23393  unconn  23394  clsconn  23395  2ndcdisj  23421  2ndcsep  23424  1stcelcls  23426  locfincmp  23491  comppfsc  23497  txcls  23569  hmphsym  23747  hmphtr  23748  hmphen  23750  haushmphlem  23752  cmphmph  23753  connhmph  23754  reghmph  23758  nrmhmph  23759  hmphdis  23761  hmphen2  23764  fbdmn0  23799  isfbas2  23800  fbssint  23803  trfbas2  23808  filtop  23820  isfil2  23821  elfg  23836  fgcl  23843  filssufilg  23876  uffix2  23889  ufildom1  23891  hauspwpwf1  23952  hausflf2  23963  alexsubALTlem2  24013  ptcmplem2  24018  cnextf  24031  tgptsmscld  24116  ustfilxp  24178  xbln0  24379  lpbl  24468  met2ndci  24487  metustfbas  24522  restmetu  24535  reconn  24794  opnreen  24797  metdsre  24819  phtpcer  24962  phtpc01  24963  phtpcco2  24966  pcohtpy  24987  cfilfcls  25241  cmetcaulem  25255  cmetcau  25256  bcthlem5  25295  ovolicc2lem2  25485  ovolicc2lem5  25488  ioorcl2  25539  ioorinv2  25542  itg11  25658  dvlip  25960  dvne0  25978  fta1g  26135  plyssc  26165  fta1  26274  vieta1lem2  26277  nobdaymin  27745  sltstr  27779  ltslpss  27900  lrrecfr  27935  oncutlt  28256  hpgerlem  28833  axcontlem4  29036  axcontlem10  29042  upgrex  29161  fusgrn0degnn0  29568  uhgrvd00  29603  wspthsnonn0vne  29985  eulerpath  30311  frgrwopreglem2  30383  ubthlem1  30941  shintcli  31400  n0limd  32541  2ndimaxp  32719  fpwrelmapffslem  32805  qsxpid  33422  qsidomlem2  33513  qsdrng  33557  1arithidom  33597  dimcl  33747  lmimdim  33748  lmicdim  33749  lvecdim0i  33750  lvecdim0  33751  lssdimle  33752  dimpropd  33753  dimkerim  33771  fedgmul  33775  extdg1id  33810  fmcncfil  34075  insiga  34281  unelldsys  34302  bnj1189  35151  bnj1279  35160  axregszf  35273  pconnconn  35413  txsconn  35423  cvmsss2  35456  cvmopnlem  35460  cvmfolem  35461  cvmliftmolem2  35464  cvmlift2lem10  35494  cvmliftpht  35500  cvmlift3lem8  35508  eldm3  35943  fundmpss  35949  elima4  35958  neibastop1  36541  neibastop2lem  36542  neibastop2  36543  fnemeet2  36549  fnejoin2  36551  neifg  36553  tailfb  36559  filnetlem3  36562  mh-infprim1bi  36728  bj-n0i  37258  bj-rest10  37400  bj-restn0  37402  poimirlem30  37971  itg2addnclem2  37993  prdsbnd2  38116  heibor1lem  38130  bfp  38145  divrngidl  38349  eldmres3  38604  rnxrn  38742  eldmxrncnvepres2  38756  trcoss2  38895  atex  39852  llnn0  39962  lplnn0N  39993  lvoln0N  40037  pmapglb2N  40217  pmapglb2xN  40218  elpaddn0  40246  osumcllem8N  40409  pexmidlem5N  40420  diaglbN  41501  diaintclN  41504  dibglbN  41612  dibintclN  41613  dihglblem2aN  41739  dihglblem5  41744  dihglbcpreN  41746  dihintcl  41790  unitscyglem5  42638  ricsym  42964  rictr  42965  riccrng1  42966  ricdrng1  42973  rencldnfilem  43248  kelac1  43491  lnmlmic  43516  gicabl  43527  neik0pk1imk0  44474  ntrneineine0lem  44510  scotteld  44673  onfrALT  44976  onfrALTVD  45317  iunconnlem2  45361  relpfrlem  45380  dfac5prim  45417  permac8prim  45441  snelmap  45513  eliin2f  45534  disjinfi  45622  mapss2  45634  difmap  45636  infrpge  45781  infxrlesupxr  45864  inficc  45964  fsumnncl  46002  ellimciota  46044  islpcn  46067  lptre2pt  46068  stoweidlem35  46463  fourierdlem31  46566  fourier2  46655  qndenserrnbllem  46722  qndenserrnopn  46726  qndenserrn  46727  intsaluni  46757  sge0cl  46809  ovn0lem  46993  ovnsubaddlem2  46999  hoidmvval0b  47018  hspdifhsp  47044  fsetprcnexALT  47510  uniimaelsetpreimafv  47856  imasetpreimafvbijlemfv1  47863  dfgric2  48391  gricuspgr  48394  gricsym  48397  grictr  48399  gricen  48401  dfgrlic2  48484  dfgrlic3  48486  grlicen  48493  gricgrlic  48494  usgrexmpl12ngric  48514  usgrexmpl12ngrlic  48515  opmpoismgm  48643  neircl  49380  sectrcl  49497  invrcl  49499  isorcl  49508  iinfssc  49532  iinfsubc  49533  imaid  49629  thincn0eu  49906  thinccic  49946  termcterm2  49989  eufunc  49997  euendfunc  50001  diag1f1o  50009  diag2f1o  50012  prstchom2ALT  50039  rellan  50098  relran  50099  alscn0d  50270