Theorem nfrab1 3443

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 3424	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		nfab1 2933	. 2 ⊢ Ⅎ𝑥{𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	1, 2	nfcxfr 2929	1 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑}

Syntax hints:   ∧ wa 400   ∈ wcel 2149  {cab 2747  Ⅎwnfc 2916  {crab 3423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-rab 3424

This theorem is referenced by:  rabss3d  4043  eqrrabd  4048  reusv2lem4  5370  reusv2  5372  rabxfrd  5386  fimarab  6953  riotaxfrd  7399  onminsb  7789  tfis  7847  oawordeulem  8535  nnawordex  8619  rankidb  9768  tskwe  9932  cardmin2  9981  cardaleph  10069  cardmin  10544  nnwos  12935  neiptopnei  23254  dissnlocfin  23651  imasnopn  23812  imasncld  23813  imasncls  23814  blval2  24684  iundisj  25672  mbfinf  25789  ltsval2  27782  lfgrnloop  29412  difrab2  32781  rabexgfGS  32782  iundisjf  32871  aciunf1  32945  fpwrelmap  33015  fpwrelmapffs  33016  iundisjfi  33078  algextdeglem6  34053  constrfin  34077  locfinreflem  34171  zarcls  34205  ordtconnlem1  34255  esumrnmpt2  34399  esumpinfval  34404  hasheuni  34416  ldsysgenld  34491  measvuni  34545  eulerpartlemn  34712  ballotlem7  34867  ballotth  34869  reprdifc  34955  bnj1230  35131  bnj1476  35176  bnj1204  35341  bnj1311  35353  onvf1odlem2  35483  vonf1oonfo  35494  satfv1  35750  bj-rabtrALT  37451  topdifinfindis  37875  icorempo  37880  isbasisrelowllem1  37884  isbasisrelowllem2  37885  relowlssretop  37892  phpreu  38138  poimirlem26  38180  poimirlem27  38181  mbfposadd  38201  cover2  38249  naddwordnexlem4  44013  rababg  44185  permaxsep  45601  rfcnpre1  45624  rfcnpre2  45636  ssrab2f  45720  infnsuprnmpt  45850  allbutfiinf  46019  supminfxr2  46068  pimxrneun  46087  limcperiod  46229  fnlimcnv  46266  fnlimfvre2  46276  fnlimf  46277  limsupequzmpt2  46317  liminfequzmpt2  46390  dvcosre  46511  stoweidlem14  46613  stoweidlem26  46625  stoweidlem31  46630  stoweidlem34  46633  stoweidlem35  46634  stoweidlem46  46645  stoweidlem50  46649  stoweidlem51  46650  stoweidlem52  46651  stoweidlem53  46652  stoweidlem54  46653  stoweidlem57  46656  stoweidlem59  46658  fourierdlem20  46726  fourierdlem31  46737  fourierdlem79  46784  sge0iunmptlemre  47014  ovnlerp  47161  opnvonmbllem1  47231  preimagelt  47298  preimalegt  47299  pimconstlt1  47301  pimltpnff  47302  pimrecltpos  47307  pimiooltgt  47309  pimdecfgtioc  47314  pimincfltioc  47315  pimdecfgtioo  47316  pimincfltioo  47317  preimageiingt  47319  preimaleiinlt  47320  pimgtmnff  47321  pimrecltneg  47323  sssmf  47337  incsmflem  47340  issmfle  47344  issmfgt  47355  smfaddlem1  47362  decsmflem  47365  issmfge  47369  smflimlem2  47371  smflim  47376  smfresal  47387  smfmullem2  47391  smfmullem4  47393  smfpimbor1lem2  47398  smflim2  47405  smfpimcclem  47406  smfsup  47413  smfinf  47417  smflimsuplem2  47420  smflimsuplem5  47423  smflimsuplem7  47425  smflimsup  47427  smfliminf  47430  smfdivdmmbl2  47440  fsupdm  47441  fsupdm2  47442  finfdm  47445  finfdm2  47446  prmdvdsfmtnof1lem1  48218