Theorem nfrab1 3001

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

Syntax hints:   /\ wa 369   e. wcel 1758   {cab 2437   F/_wnfc 2600   {crab 2800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794  ax-13 1954  ax-ext 2431

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-rab 2805

This theorem is referenced by:  reusv2lem4  4599  reusv2  4601  reusv6OLD  4606  rabxfrd  4616  riotaxfrd  6187  onminsb  6515  tfis  6570  oawordeulem  7098  nnawordex  7181  rankidb  8113  tskwe  8226  cardmin2  8274  cardaleph  8365  cardmin  8834  nnwos  11028  neiptopnei  18863  imasnopn  19390  imasncld  19391  imasncls  19392  blval2  20277  iundisj  21157  mbfinf  21271  rabexgfGS  26033  rabss3d  26042  iundisjf  26077  fpwrelmap  26179  fpwrelmapffs  26180  iundisjfi  26220  ordtconlem1  26494  esumpinfval  26662  hasheuni  26674  measvuni  26768  eulerpartlemn  26903  ballotlem7  27057  ballotth  27059  sltval2  27936  nobndlem5  27976  mbfposadd  28582  dvtanlem  28584  cover2  28750  rfcnpre1  29884  rfcnpre2  29896  dvcosre  29931  stoweidlem14  29952  stoweidlem26  29964  stoweidlem31  29969  stoweidlem34  29972  stoweidlem35  29973  stoweidlem46  29984  stoweidlem50  29988  stoweidlem51  29989  stoweidlem52  29990  stoweidlem53  29991  stoweidlem54  29992  stoweidlem57  29995  stoweidlem59  29997  bnj1230  32109  bnj1476  32153  bnj1204  32316  bnj1311  32328  bj-rabtrALT  32746