Theorem nfrab1 3337

Description: The abstraction variable in a restricted class abstraction isn't free. (Contributed by NM, 19-Mar-1997.)

Assertion

Ref	Expression
nfrab1	⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑}

Proof of Theorem nfrab1

Step	Hyp	Ref	Expression
1		df-rab 3115	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		nfab1 2957	. 2 ⊢ Ⅎ𝑥{𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	1, 2	nfcxfr 2953	1 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑}

Syntax hints:   ∧ wa 399   ∈ wcel 2111  {cab 2776  Ⅎwnfc 2936  {crab 3110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115

This theorem is referenced by:  reusv2lem4  5267  reusv2  5269  rabxfrd  5283  riotaxfrd  7127  onminsb  7494  tfis  7549  oawordeulem  8163  nnawordex  8246  rankidb  9213  tskwe  9363  cardmin2  9412  cardaleph  9500  cardmin  9975  nnwos  12303  neiptopnei  21737  dissnlocfin  22134  imasnopn  22295  imasncld  22296  imasncls  22297  blval2  23169  iundisj  24152  mbfinf  24269  lfgrnloop  26918  difrab2  30268  rabexgfGS  30269  eqrrabd  30272  rabss3d  30285  iundisjf  30352  fimarab  30404  aciunf1  30426  fpwrelmap  30495  fpwrelmapffs  30496  iundisjfi  30545  locfinreflem  31193  zarcls  31227  ordtconnlem1  31277  esumrnmpt2  31437  esumpinfval  31442  hasheuni  31454  ldsysgenld  31529  measvuni  31583  eulerpartlemn  31749  ballotlem7  31903  ballotth  31905  reprdifc  32008  bnj1230  32184  bnj1476  32229  bnj1204  32394  bnj1311  32406  satfv1  32723  sltval2  33276  bj-rabtrALT  34373  topdifinfindis  34763  icorempo  34768  isbasisrelowllem1  34772  isbasisrelowllem2  34773  relowlssretop  34780  phpreu  35041  poimirlem26  35083  poimirlem27  35084  mbfposadd  35104  cover2  35152  rababg  40273  rfcnpre1  41648  rfcnpre2  41660  ssrab2f  41752  infnsuprnmpt  41888  allbutfiinf  42057  supminfxr2  42108  fsumiunss  42217  limcperiod  42270  fnlimcnv  42309  fnlimfvre2  42319  fnlimf  42320  limsupequzmpt2  42360  liminfequzmpt2  42433  dvcosre  42554  stoweidlem14  42656  stoweidlem26  42668  stoweidlem31  42673  stoweidlem34  42676  stoweidlem35  42677  stoweidlem46  42688  stoweidlem50  42692  stoweidlem51  42693  stoweidlem52  42694  stoweidlem53  42695  stoweidlem54  42696  stoweidlem57  42699  stoweidlem59  42701  fourierdlem20  42769  fourierdlem31  42780  fourierdlem79  42827  sge0iunmptlemre  43054  ovnlerp  43201  opnvonmbllem1  43271  preimagelt  43337  preimalegt  43338  pimconstlt1  43340  pimltpnf  43341  pimrecltpos  43344  pimiooltgt  43346  pimdecfgtioc  43350  pimincfltioc  43351  pimdecfgtioo  43352  pimincfltioo  43353  preimageiingt  43355  preimaleiinlt  43356  pimrecltneg  43358  sssmf  43372  incsmflem  43375  issmfle  43379  issmfgt  43390  smfaddlem1  43396  decsmflem  43399  issmfge  43403  smflimlem2  43405  smflim  43410  smfresal  43420  smfmullem2  43424  smfmullem4  43426  smfpimbor1lem2  43431  smflim2  43437  smfpimcclem  43438  smfsup  43445  smfinf  43449  smflimsuplem2  43452  smflimsuplem5  43455  smflimsuplem7  43457  smflimsup  43459  smfliminf  43462  prmdvdsfmtnof1lem1  44101