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

Theorem nfrab1 2733
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 2565 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 nfab1 2434 . 2  |-  F/_ x { x  |  (
x  e.  A  /\  ph ) }
31, 2nfcxfr 2429 1  |-  F/_ x { x  e.  A  |  ph }
Colors of variables: wff set class
Syntax hints:    /\ wa 358    e. wcel 1696   {cab 2282   F/_wnfc 2419   {crab 2560
This theorem is referenced by:  reusv2lem4  4554  reusv2  4556  reusv6OLD  4561  rabxfrd  4571  onminsb  4606  tfis  4661  riotaxfrd  6352  oawordeulem  6568  nnawordex  6651  rankidb  7488  tskwe  7599  cardmin2  7647  cardaleph  7732  cardmin  8202  nnwos  10302  iundisj  18921  mbfinf  19036  ballotlem7  23110  ballotth  23112  rabss3d  23152  rabexgfGS  23187  iundisjfi  23378  iundisjf  23380  esumpinfval  23456  hasheuni  23468  measvuni  23557  sltval2  24381  nobndlem5  24421  sgplpte21a  26236  cover2  26461  rfcnpre1  27793  rfcnpre2  27805  dvcosre  27844  stoweidlem14  27866  stoweidlem26  27878  stoweidlem31  27883  stoweidlem34  27886  stoweidlem35  27887  stoweidlem46  27898  stoweidlem50  27902  stoweidlem51  27903  stoweidlem52  27904  stoweidlem53  27905  stoweidlem54  27906  stoweidlem57  27909  stoweidlem59  27911  bnj1230  29151  bnj1476  29195  bnj1204  29358  bnj1311  29370
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565
  Copyright terms: Public domain W3C validator