Theorem nfrab1 3016

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

Syntax hints:   /\ wa 370   e. wcel 1870   {cab 2414   F/_wnfc 2577   {crab 2786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791

This theorem is referenced by:  reusv2lem4  4629  reusv2  4631  rabxfrd  4643  riotaxfrd  6297  onminsb  6640  tfis  6695  oawordeulem  7263  nnawordex  7346  rankidb  8270  tskwe  8383  cardmin2  8431  cardaleph  8518  cardmin  8987  nnwos  11226  neiptopnei  20083  dissnlocfin  20479  imasnopn  20640  imasncld  20641  imasncls  20642  blval2  21512  iundisj  22386  mbfinf  22506  mbfinfOLD  22507  rabexgfGS  27981  rabss3d  27992  iundisjf  28046  fimarab  28092  aciunf1  28113  fpwrelmap  28169  fpwrelmapffs  28170  iundisjfi  28216  locfinreflem  28514  ordtconlem1  28577  esumrnmpt2  28736  esumpinfval  28741  hasheuni  28753  ldsysgenld  28829  measvuni  28883  eulerpartlemn  29048  ballotlem7  29202  ballotth  29204  bnj1230  29410  bnj1476  29454  bnj1204  29617  bnj1311  29629  sltval2  30338  nobndlem5  30378  bj-rabtrALT  31292  topdifinfindis  31491  icorempt2  31496  isbasisrelowllem1  31500  isbasisrelowllem2  31501  relowlssretop  31508  phpreu  31644  poimirlem26  31681  poimirlem27  31682  mbfposadd  31703  dvtanlemOLD  31706  cover2  31755  rfcnpre1  36995  rfcnpre2  37007  fsumiunss  37244  limcperiod  37295  dvcosre  37368  stoweidlem14  37458  stoweidlem26  37470  stoweidlem31  37476  stoweidlem34  37479  stoweidlem35  37480  stoweidlem46  37491  stoweidlem50  37495  stoweidlem51  37496  stoweidlem52  37497  stoweidlem53  37498  stoweidlem54  37499  stoweidlem57  37502  stoweidlem59  37504  fourierdlem20  37573  fourierdlem31  37584  fourierdlem79  37632  sge0iunmptlemre  37806