MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rabn0 Structured version   Visualization version   GIF version

Theorem rabn0 3991
Description: Nonempty restricted class abstraction. (Contributed by NM, 29-Aug-1999.) (Revised by BJ, 16-Jul-2021.)
Assertion
Ref Expression
rabn0 ({𝑥𝐴𝜑} ≠ ∅ ↔ ∃𝑥𝐴 𝜑)

Proof of Theorem rabn0
StepHypRef Expression
1 rabeq0 3990 . . 3 ({𝑥𝐴𝜑} = ∅ ↔ ∀𝑥𝐴 ¬ 𝜑)
21necon3abii 2869 . 2 ({𝑥𝐴𝜑} ≠ ∅ ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
3 dfrex2 3025 . 2 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
42, 3bitr4i 267 1 ({𝑥𝐴𝜑} ≠ ∅ ↔ ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wne 2823  wral 2941  wrex 2942  {crab 2945  c0 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-nul 3949
This theorem is referenced by:  class2set  4862  reusv2  4904  exss  4961  frminex  5123  weniso  6644  onminesb  7040  onminsb  7041  onminex  7049  oeeulem  7726  supval2  8402  ordtypelem3  8466  card2on  8500  tz9.12lem3  8690  rankf  8695  scott0  8787  karden  8796  cardf2  8807  cardval3  8816  cardmin2  8862  acni3  8908  kmlem3  9012  cofsmo  9129  coftr  9133  fin23lem7  9176  enfin2i  9181  axcc4  9299  axdc3lem4  9313  ac6num  9339  pwfseqlem3  9520  wuncval  9602  wunccl  9604  tskmcl  9701  infm3  11020  nnwos  11793  zsupss  11815  zmin  11822  rpnnen1lem2  11852  rpnnen1lem1  11853  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem1OLD  11859  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  ioo0  12238  ico0  12259  ioc0  12260  icc0  12261  bitsfzolem  15203  lcmcllem  15356  fissn0dvdsn0  15380  odzcllem  15544  vdwnn  15749  ram0  15773  ramsey  15781  sylow2blem3  18083  iscyg2  18330  pgpfac1lem5  18524  ablfaclem2  18531  ablfaclem3  18532  ablfac  18533  lspf  19022  ordtrest2lem  21055  ordthauslem  21235  1stcfb  21296  2ndcdisj  21307  ptclsg  21466  txconn  21540  txflf  21857  tsmsfbas  21978  iscmet3  23137  minveclem3b  23245  iundisj  23362  dyadmax  23412  dyadmbllem  23413  elqaalem1  24119  elqaalem3  24121  sgmnncl  24918  musum  24962  incistruhgr  26019  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  spancl  28323  shsval2i  28374  ococin  28395  iundisjf  29528  iundisjfi  29683  ordtrest2NEWlem  30096  esumrnmpt2  30258  esumpinfval  30263  dmsigagen  30335  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemiex  30691  ballotlemsup  30694  bnj110  31054  bnj1204  31206  bnj1253  31211  connpconn  31343  iscvm  31367  wsuclem  31895  conway  32035  poimirlem28  33567  sstotbnd2  33703  igenval  33990  igenidl  33992  pmap0  35369  pellfundre  37762  pellfundge  37763  pellfundglb  37766  dgraalem  38032  rgspncl  38056  uzwo4  39535  ioodvbdlimc1lem1  40464  fourierdlem31  40673  fourierdlem64  40705  etransclem48  40817  subsaliuncl  40894  smflimlem6  41305  smfpimcc  41335  prmdvdsfmtnof1lem1  41821  prmdvdsfmtnof  41823
  Copyright terms: Public domain W3C validator