MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfrab1 Structured version   Unicode version

Theorem nfrab1 2888
Description: The abstraction variable in a restricted class abstraction isn't free. (Contributed by NM, 19-Mar-1997.)
Assertion
Ref Expression
nfrab1  |-  F/_ x { x  e.  A  |  ph }

Proof of Theorem nfrab1
StepHypRef Expression
1 df-rab 2714 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 nfab1 2574 . 2  |-  F/_ x { x  |  (
x  e.  A  /\  ph ) }
31, 2nfcxfr 2569 1  |-  F/_ x { x  e.  A  |  ph }
Colors of variables: wff set class
Syntax hints:    /\ wa 359    e. wcel 1725   {cab 2422   F/_wnfc 2559   {crab 2709
This theorem is referenced by:  reusv2lem4  4727  reusv2  4729  reusv6OLD  4734  rabxfrd  4744  onminsb  4779  tfis  4834  riotaxfrd  6581  oawordeulem  6797  nnawordex  6880  rankidb  7726  tskwe  7837  cardmin2  7885  cardaleph  7970  cardmin  8439  nnwos  10544  neiptopnei  17196  imasnopn  17722  imasncld  17723  imasncls  17724  blval2  18605  iundisj  19442  mbfinf  19557  rabexgfGS  23987  rabss3d  23995  iundisjf  24029  iundisjfi  24152  esumpinfval  24463  hasheuni  24475  measvuni  24568  ballotlem7  24793  ballotth  24795  sltval2  25611  nobndlem5  25651  mbfposadd  26254  cover2  26415  rfcnpre1  27666  rfcnpre2  27678  dvcosre  27717  stoweidlem14  27739  stoweidlem26  27751  stoweidlem31  27756  stoweidlem34  27759  stoweidlem35  27760  stoweidlem46  27771  stoweidlem50  27775  stoweidlem51  27776  stoweidlem52  27777  stoweidlem53  27778  stoweidlem54  27779  stoweidlem57  27782  stoweidlem59  27784  bnj1230  29174  bnj1476  29218  bnj1204  29381  bnj1311  29393
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714
  Copyright terms: Public domain W3C validator