Theorem nfrab1 2983

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

Syntax hints:   /\ wa 375   e. wcel 1898   {cab 2448   F/_wnfc 2590   {crab 2753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758

This theorem is referenced by:  reusv2lem4  4621  reusv2  4623  rabxfrd  4635  riotaxfrd  6307  onminsb  6653  tfis  6708  oawordeulem  7281  nnawordex  7364  rankidb  8297  tskwe  8410  cardmin2  8458  cardaleph  8546  cardmin  9015  nnwos  11255  neiptopnei  20197  dissnlocfin  20593  imasnopn  20754  imasncld  20755  imasncls  20756  blval2  21626  iundisj  22550  mbfinf  22670  mbfinfOLD  22671  rabexgfGS  28186  rabss3d  28197  iundisjf  28248  fimarab  28293  aciunf1  28314  fpwrelmap  28367  fpwrelmapffs  28368  iundisjfi  28421  locfinreflem  28716  ordtconlem1  28779  esumrnmpt2  28938  esumpinfval  28943  hasheuni  28955  ldsysgenld  29031  measvuni  29085  eulerpartlemn  29263  ballotlem7  29417  ballotth  29419  ballotlem7OLD  29455  ballotthOLD  29457  bnj1230  29663  bnj1476  29707  bnj1204  29870  bnj1311  29882  sltval2  30592  nobndlem5  30634  bj-rabtrALT  31579  topdifinfindis  31794  icorempt2  31799  isbasisrelowllem1  31803  isbasisrelowllem2  31804  relowlssretop  31811  phpreu  31974  poimirlem26  32011  poimirlem27  32012  mbfposadd  32033  dvtanlemOLD  32036  cover2  32085  rababg  36224  rfcnpre1  37380  rfcnpre2  37392  fsumiunss  37692  limcperiod  37746  dvcosre  37819  stoweidlem14  37912  stoweidlem26  37924  stoweidlem31  37930  stoweidlem34  37933  stoweidlem35  37934  stoweidlem46  37945  stoweidlem50  37949  stoweidlem51  37950  stoweidlem52  37951  stoweidlem53  37952  stoweidlem54  37953  stoweidlem57  37956  stoweidlem59  37958  fourierdlem20  38027  fourierdlem31  38038  fourierdlem31OLD  38039  fourierdlem79  38087  sge0iunmptlemre  38295  ovnlerp  38422  opnvonmbllem1  38492