Theorem nfrab1 3122

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

Syntax hints:   /\ wa 384   e. wcel 1990   {cab 2608   F/_wnfc 2751   {crab 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921

This theorem is referenced by:  reusv2lem4  4872  reusv2  4874  rabxfrd  4889  riotaxfrd  6642  onminsb  6999  tfis  7054  oawordeulem  7634  nnawordex  7717  rankidb  8663  tskwe  8776  cardmin2  8824  cardaleph  8912  cardmin  9386  nnwos  11755  neiptopnei  20936  dissnlocfin  21332  imasnopn  21493  imasncld  21494  imasncls  21495  blval2  22367  iundisj  23316  mbfinf  23432  lfgrnloop  26020  numclwlk1lem2  27230  difrab2  29339  rabexgfGS  29340  rabss3d  29351  iundisjf  29402  fimarab  29445  aciunf1  29463  fpwrelmap  29508  fpwrelmapffs  29509  iundisjfi  29555  locfinreflem  29907  ordtconnlem1  29970  esumrnmpt2  30130  esumpinfval  30135  hasheuni  30147  ldsysgenld  30223  measvuni  30277  eulerpartlemn  30443  ballotlem7  30597  ballotth  30599  reprdifc  30705  bnj1230  30873  bnj1476  30917  bnj1204  31080  bnj1311  31092  sltval2  31809  bj-rabtrALT  32927  topdifinfindis  33194  icorempt2  33199  isbasisrelowllem1  33203  isbasisrelowllem2  33204  relowlssretop  33211  phpreu  33393  poimirlem26  33435  poimirlem27  33436  mbfposadd  33457  cover2  33508  rababg  37879  rfcnpre1  39178  rfcnpre2  39190  ssrab2f  39300  infnsuprnmpt  39465  allbutfiinf  39647  supminfxr2  39699  fsumiunss  39807  limcperiod  39860  fnlimcnv  39899  fnlimfvre2  39909  fnlimf  39910  limsupequzmpt2  39950  liminfequzmpt2  40023  dvcosre  40126  stoweidlem14  40231  stoweidlem26  40243  stoweidlem31  40248  stoweidlem34  40251  stoweidlem35  40252  stoweidlem46  40263  stoweidlem50  40267  stoweidlem51  40268  stoweidlem52  40269  stoweidlem53  40270  stoweidlem54  40271  stoweidlem57  40274  stoweidlem59  40276  fourierdlem20  40344  fourierdlem31  40355  fourierdlem79  40402  sge0iunmptlemre  40632  ovnlerp  40776  opnvonmbllem1  40846  preimagelt  40912  preimalegt  40913  pimconstlt1  40915  pimltpnf  40916  pimrecltpos  40919  pimiooltgt  40921  pimdecfgtioc  40925  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  preimageiingt  40930  preimaleiinlt  40931  pimrecltneg  40933  sssmf  40947  incsmflem  40950  issmfle  40954  issmfgt  40965  smfaddlem1  40971  decsmflem  40974  issmfge  40978  smflimlem2  40980  smflim  40985  smfresal  40995  smfmullem2  40999  smfmullem4  41001  smfpimbor1lem2  41006  smflim2  41012  smfpimcclem  41013  smfsup  41020  smfinf  41024  smflimsuplem2  41027  smflimsuplem3  41028  smflimsuplem5  41030  smflimsuplem7  41032  smflimsup  41034  smfliminf  41037  prmdvdsfmtnof1lem1  41496