Theorem nfrab1 2891

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

Syntax hints:   /\ wa 369   e. wcel 1755   {cab 2419   F/_wnfc 2556   {crab 2709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714

This theorem is referenced by:  reusv2lem4  4484  reusv2  4486  reusv6OLD  4491  rabxfrd  4501  riotaxfrd  6071  onminsb  6399  tfis  6454  oawordeulem  6981  nnawordex  7064  rankidb  7995  tskwe  8108  cardmin2  8156  cardaleph  8247  cardmin  8716  nnwos  10909  neiptopnei  18577  imasnopn  19104  imasncld  19105  imasncls  19106  blval2  19991  iundisj  20870  mbfinf  20984  rabexgfGS  25709  rabss3d  25718  iundisjf  25754  fpwrelmap  25857  fpwrelmapffs  25858  iundisjfi  25902  ordtconlem1  26207  esumpinfval  26375  hasheuni  26387  measvuni  26481  eulerpartlemn  26611  ballotlem7  26765  ballotth  26767  sltval2  27643  nobndlem5  27683  mbfposadd  28280  dvtanlem  28282  cover2  28448  rfcnpre1  29583  rfcnpre2  29595  dvcosre  29631  stoweidlem14  29652  stoweidlem26  29664  stoweidlem31  29669  stoweidlem34  29672  stoweidlem35  29673  stoweidlem46  29684  stoweidlem50  29688  stoweidlem51  29689  stoweidlem52  29690  stoweidlem53  29691  stoweidlem54  29692  stoweidlem57  29695  stoweidlem59  29697  bnj1230  31495  bnj1476  31539  bnj1204  31702  bnj1311  31714  bj-rabtrALT  32016