Theorem nfrab1 3433

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

Syntax hints:   ∧ wa 399   ∈ wcel 2141  {cab 2739  Ⅎwnfc 2908  {crab 3413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-rab 3414

This theorem is referenced by:  rabss3d  4032  eqrrabd  4037  reusv2lem4  5355  reusv2  5357  rabxfrd  5371  fimarab  6936  riotaxfrd  7382  onminsb  7772  tfis  7830  oawordeulem  8517  nnawordex  8601  rankidb  9752  tskwe  9902  cardmin2  9951  cardaleph  10039  cardmin  10515  nnwos  12910  neiptopnei  23180  dissnlocfin  23577  imasnopn  23738  imasncld  23739  imasncls  23740  blval2  24610  iundisj  25598  mbfinf  25715  ltsval2  27708  lfgrnloop  29283  difrab2  32656  rabexgfGS  32658  iundisjf  32749  aciunf1  32826  fpwrelmap  32896  fpwrelmapffs  32897  iundisjfi  32959  algextdeglem6  33980  constrfin  34004  locfinreflem  34098  zarcls  34132  ordtconnlem1  34182  esumrnmpt2  34326  esumpinfval  34331  hasheuni  34343  ldsysgenld  34418  measvuni  34472  eulerpartlemn  34639  ballotlem7  34794  ballotth  34796  reprdifc  34882  bnj1230  35058  bnj1476  35103  bnj1204  35268  bnj1311  35280  onvf1odlem2  35408  vonf1oonfo  35419  satfv1  35674  bj-rabtrALT  37377  topdifinfindis  37801  icorempo  37806  isbasisrelowllem1  37810  isbasisrelowllem2  37811  relowlssretop  37818  phpreu  38064  poimirlem26  38106  poimirlem27  38107  mbfposadd  38127  cover2  38175  naddwordnexlem4  43939  rababg  44111  permaxsep  45544  rfcnpre1  45560  rfcnpre2  45572  ssrab2f  45656  infnsuprnmpt  45786  allbutfiinf  45955  supminfxr2  46004  pimxrneun  46023  limcperiod  46165  fnlimcnv  46202  fnlimfvre2  46212  fnlimf  46213  limsupequzmpt2  46253  liminfequzmpt2  46326  dvcosre  46447  stoweidlem14  46549  stoweidlem26  46561  stoweidlem31  46566  stoweidlem34  46569  stoweidlem35  46570  stoweidlem46  46581  stoweidlem50  46585  stoweidlem51  46586  stoweidlem52  46587  stoweidlem53  46588  stoweidlem54  46589  stoweidlem57  46592  stoweidlem59  46594  fourierdlem20  46662  fourierdlem31  46673  fourierdlem79  46720  sge0iunmptlemre  46950  ovnlerp  47097  opnvonmbllem1  47167  preimagelt  47234  preimalegt  47235  pimconstlt1  47237  pimltpnff  47238  pimrecltpos  47243  pimiooltgt  47245  pimdecfgtioc  47250  pimincfltioc  47251  pimdecfgtioo  47252  pimincfltioo  47253  preimageiingt  47255  preimaleiinlt  47256  pimgtmnff  47257  pimrecltneg  47259  sssmf  47273  incsmflem  47276  issmfle  47280  issmfgt  47291  smfaddlem1  47298  decsmflem  47301  issmfge  47305  smflimlem2  47307  smflim  47312  smfresal  47323  smfmullem2  47327  smfmullem4  47329  smfpimbor1lem2  47334  smflim2  47341  smfpimcclem  47342  smfsup  47349  smfinf  47353  smflimsuplem2  47356  smflimsuplem5  47359  smflimsuplem7  47361  smflimsup  47363  smfliminf  47366  smfdivdmmbl2  47376  fsupdm  47377  fsupdm2  47378  finfdm  47381  finfdm2  47382  prmdvdsfmtnof1lem1  48154