Theorem nfrab1 2848

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

Step	Hyp	Ref	Expression
1		df-rab 2675	. 2 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
2		nfab1 2542	. 2 |- F/_ x { x | ( x e. A /\ ph ) }
3	1, 2	nfcxfr 2537	1 |- F/_ x { x e. A | ph }

Syntax hints:   /\ wa 359   e. wcel 1721   {cab 2390   F/_wnfc 2527   {crab 2670

This theorem is referenced by:  reusv2lem4  4686  reusv2  4688  reusv6OLD  4693  rabxfrd  4703  onminsb  4738  tfis  4793  riotaxfrd  6540  oawordeulem  6756  nnawordex  6839  rankidb  7682  tskwe  7793  cardmin2  7841  cardaleph  7926  cardmin  8395  nnwos  10500  neiptopnei  17151  imasnopn  17675  imasncld  17676  imasncls  17677  blval2  18558  iundisj  19395  mbfinf  19510  rabexgfGS  23940  rabss3d  23948  iundisjf  23982  iundisjfi  24105  esumpinfval  24416  hasheuni  24428  measvuni  24521  ballotlem7  24746  ballotth  24748  sltval2  25524  nobndlem5  25564  mbfposadd  26153  cover2  26305  rfcnpre1  27557  rfcnpre2  27569  dvcosre  27608  stoweidlem14  27630  stoweidlem26  27642  stoweidlem31  27647  stoweidlem34  27650  stoweidlem35  27651  stoweidlem46  27662  stoweidlem50  27666  stoweidlem51  27667  stoweidlem52  27668  stoweidlem53  27669  stoweidlem54  27670  stoweidlem57  27673  stoweidlem59  27675  bnj1230  28880  bnj1476  28924  bnj1204  29087  bnj1311  29099

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675