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

Theorem nfrab1 2720
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 2552 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 nfab1 2421 . 2  |-  F/_ x { x  |  (
x  e.  A  /\  ph ) }
31, 2nfcxfr 2416 1  |-  F/_ x { x  e.  A  |  ph }
Colors of variables: wff set class
Syntax hints:    /\ wa 358    e. wcel 1684   {cab 2269   F/_wnfc 2406   {crab 2547
This theorem is referenced by:  reusv2lem4  4538  reusv2  4540  reusv6OLD  4545  rabxfrd  4555  onminsb  4590  tfis  4645  riotaxfrd  6336  oawordeulem  6552  nnawordex  6635  rankidb  7472  tskwe  7583  cardmin2  7631  cardaleph  7716  cardmin  8186  nnwos  10286  iundisj  18905  mbfinf  19020  ballotlem7  23094  ballotth  23096  rabss3d  23136  rabexgfGS  23171  iundisjfi  23363  iundisjf  23365  esumpinfval  23441  hasheuni  23453  measvuni  23542  sltval2  24310  nobndlem5  24350  sgplpte21a  26133  cover2  26358  rfcnpre1  27690  rfcnpre2  27702  dvcosre  27741  stoweidlem14  27763  stoweidlem26  27775  stoweidlem31  27780  stoweidlem34  27783  stoweidlem35  27784  stoweidlem46  27795  stoweidlem50  27799  stoweidlem51  27800  stoweidlem52  27801  stoweidlem53  27802  stoweidlem54  27803  stoweidlem57  27806  stoweidlem59  27808  bnj1230  28835  bnj1476  28879  bnj1204  29042  bnj1311  29054
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552
  Copyright terms: Public domain W3C validator