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

Theorem rabn0 4338
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 4337 . . 3 ({𝑥𝐴𝜑} = ∅ ↔ ∀𝑥𝐴 ¬ 𝜑)
21necon3abii 3062 . 2 ({𝑥𝐴𝜑} ≠ ∅ ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
3 dfrex2 3239 . 2 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
42, 3bitr4i 279 1 ({𝑥𝐴𝜑} ≠ ∅ ↔ ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207  wne 3016  wral 3138  wrex 3139  {crab 3142  c0 4290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-dif 3938  df-nul 4291
This theorem is referenced by:  class2set  5246  reusv2  5295  exss  5347  frminex  5529  weniso  7096  onminesb  7501  onminsb  7502  onminex  7510  oeeulem  8217  supval2  8908  ordtypelem3  8973  card2on  9007  tz9.12lem3  9207  rankf  9212  scott0  9304  karden  9313  cardf2  9361  cardval3  9370  cardmin2  9416  acni3  9462  kmlem3  9567  cofsmo  9680  coftr  9684  fin23lem7  9727  enfin2i  9732  axcc4  9850  axdc3lem4  9864  ac6num  9890  pwfseqlem3  10071  wuncval  10153  wunccl  10155  tskmcl  10252  infm3  11589  nnwos  12304  zsupss  12326  zmin  12333  rpnnen1lem2  12366  rpnnen1lem1  12367  rpnnen1lem3  12368  rpnnen1lem5  12370  ioo0  12753  ico0  12774  ioc0  12775  icc0  12776  bitsfzolem  15773  lcmcllem  15930  fissn0dvdsn0  15954  odzcllem  16119  vdwnn  16324  ram0  16348  ramsey  16356  sylow2blem3  18678  iscyg2  18932  pgpfac1lem5  19132  ablfaclem2  19139  ablfaclem3  19140  ablfac  19141  lspf  19677  ordtrest2lem  21741  ordthauslem  21921  1stcfb  21983  2ndcdisj  21994  ptclsg  22153  txconn  22227  txflf  22544  tsmsfbas  22665  iscmet3  23825  minveclem3b  23960  iundisj  24078  dyadmax  24128  dyadmbllem  24129  elqaalem1  24837  elqaalem3  24839  sgmnncl  25652  musum  25696  incistruhgr  26792  uvtx01vtx  27107  spancl  29041  shsval2i  29092  ococin  29113  iundisjf  30268  iundisjfi  30446  ordtrest2NEWlem  31065  esumrnmpt2  31227  esumpinfval  31232  dmsigagen  31303  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemiex  31659  ballotlemsup  31662  bnj110  32030  bnj1204  32182  bnj1253  32187  connpconn  32380  iscvm  32404  wsuclem  33010  conway  33162  poimirlem28  34802  sstotbnd2  34935  igenval  35222  igenidl  35224  pmap0  36783  pellfundre  39358  pellfundge  39359  pellfundglb  39362  dgraalem  39625  rgspncl  39649  uzwo4  41195  ioodvbdlimc1lem1  42096  fourierdlem31  42304  fourierdlem64  42336  etransclem48  42448  subsaliuncl  42522  smflimlem6  42933  smfpimcc  42963  prmdvdsfmtnof1lem1  43593  prmdvdsfmtnof  43595
  Copyright terms: Public domain W3C validator