Theorem nfrab1 3042

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 2823	. 2 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
2		nfab1 2631	. 2 |- F/_ x { x | ( x e. A /\ ph ) }
3	1, 2	nfcxfr 2627	1 |- F/_ x { x e. A | ph }

Syntax hints:   /\ wa 369   e. wcel 1767   {cab 2452   F/_wnfc 2615   {crab 2818

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823

This theorem is referenced by:  reusv2lem4  4651  reusv2  4653  reusv6OLD  4658  rabxfrd  4668  riotaxfrd  6274  onminsb  6612  tfis  6667  oawordeulem  7200  nnawordex  7283  rankidb  8214  tskwe  8327  cardmin2  8375  cardaleph  8466  cardmin  8935  nnwos  11145  neiptopnei  19399  imasnopn  19926  imasncld  19927  imasncls  19928  blval2  20813  iundisj  21693  mbfinf  21807  rabexgfGS  27077  rabss3d  27086  iundisjf  27121  fpwrelmap  27228  fpwrelmapffs  27229  iundisjfi  27269  ordtconlem1  27542  esumpinfval  27719  hasheuni  27731  measvuni  27825  eulerpartlemn  27960  ballotlem7  28114  ballotth  28116  sltval2  28993  nobndlem5  29033  mbfposadd  29639  dvtanlem  29641  cover2  29807  rfcnpre1  30972  rfcnpre2  30984  limcperiod  31170  dvcosre  31239  stoweidlem14  31314  stoweidlem26  31326  stoweidlem31  31331  stoweidlem34  31334  stoweidlem35  31335  stoweidlem46  31346  stoweidlem50  31350  stoweidlem51  31351  stoweidlem52  31352  stoweidlem53  31353  stoweidlem54  31354  stoweidlem57  31357  stoweidlem59  31359  fourierdlem20  31427  fourierdlem31  31438  fourierdlem79  31486  bnj1230  32940  bnj1476  32984  bnj1204  33147  bnj1311  33159  bj-rabtrALT  33579