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

Theorem rabn0 4124
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 4123 . . 3 ({𝑥𝐴𝜑} = ∅ ↔ ∀𝑥𝐴 ¬ 𝜑)
21necon3abii 2983 . 2 ({𝑥𝐴𝜑} ≠ ∅ ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
3 dfrex2 3142 . 2 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
42, 3bitr4i 269 1 ({𝑥𝐴𝜑} ≠ ∅ ↔ ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197  wne 2937  wral 3055  wrex 3056  {crab 3059  c0 4081
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3737  df-nul 4082
This theorem is referenced by:  class2set  4992  reusv2  5040  exss  5089  frminex  5259  weniso  6800  onminesb  7200  onminsb  7201  onminex  7209  oeeulem  7890  supval2  8572  ordtypelem3  8636  card2on  8670  tz9.12lem3  8871  rankf  8876  scott0  8968  karden  8977  cardf2  9024  cardval3  9033  cardmin2  9079  acni3  9125  kmlem3  9231  cofsmo  9348  coftr  9352  fin23lem7  9395  enfin2i  9400  axcc4  9518  axdc3lem4  9532  ac6num  9558  pwfseqlem3  9739  wuncval  9821  wunccl  9823  tskmcl  9920  infm3  11240  nnwos  11961  zsupss  11983  zmin  11990  rpnnen1lem2  12020  rpnnen1lem1  12021  rpnnen1lem3  12022  rpnnen1lem5  12024  ioo0  12407  ico0  12428  ioc0  12429  icc0  12430  bitsfzolem  15451  lcmcllem  15604  fissn0dvdsn0  15628  odzcllem  15790  vdwnn  15995  ram0  16019  ramsey  16027  sylow2blem3  18315  iscyg2  18564  pgpfac1lem5  18759  ablfaclem2  18766  ablfaclem3  18767  ablfac  18768  lspf  19260  ordtrest2lem  21301  ordthauslem  21481  1stcfb  21542  2ndcdisj  21553  ptclsg  21712  txconn  21786  txflf  22103  tsmsfbas  22224  iscmet3  23384  minveclem3b  23502  iundisj  23620  dyadmax  23670  dyadmbllem  23671  elqaalem1  24379  elqaalem3  24381  sgmnncl  25178  musum  25222  incistruhgr  26265  uvtx01vtx  26595  uvtxa01vtx0OLD  26597  spancl  28672  shsval2i  28723  ococin  28744  iundisjf  29871  iundisjfi  30025  ordtrest2NEWlem  30436  esumrnmpt2  30598  esumpinfval  30603  dmsigagen  30675  ballotlemfc0  31023  ballotlemfcc  31024  ballotlemiex  31032  ballotlemsup  31035  bnj110  31397  bnj1204  31549  bnj1253  31554  connpconn  31686  iscvm  31710  wsuclem  32235  conway  32375  poimirlem28  33882  sstotbnd2  34016  igenval  34303  igenidl  34305  pmap0  35742  pellfundre  38147  pellfundge  38148  pellfundglb  38151  dgraalem  38416  rgspncl  38440  uzwo4  39896  ioodvbdlimc1lem1  40808  fourierdlem31  41016  fourierdlem64  41048  etransclem48  41160  subsaliuncl  41237  smflimlem6  41648  smfpimcc  41678  prmdvdsfmtnof1lem1  42196  prmdvdsfmtnof  42198
  Copyright terms: Public domain W3C validator