Theorem nfrab1 3415

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

Syntax hints:   ∧ wa 395   ∈ wcel 2111  {cab 2709  Ⅎwnfc 2879  {crab 3395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-rab 3396

This theorem is referenced by:  rabss3d  4026  eqrrabd  4031  reusv2lem4  5334  reusv2  5336  rabxfrd  5350  fimarab  6891  riotaxfrd  7332  onminsb  7722  tfis  7780  oawordeulem  8464  nnawordex  8547  rankidb  9688  tskwe  9838  cardmin2  9887  cardaleph  9975  cardmin  10450  nnwos  12808  neiptopnei  23042  dissnlocfin  23439  imasnopn  23600  imasncld  23601  imasncls  23602  blval2  24472  iundisj  25471  mbfinf  25588  sltval2  27590  lfgrnloop  29098  difrab2  32469  rabexgfGS  32471  iundisjf  32561  aciunf1  32637  fpwrelmap  32708  fpwrelmapffs  32709  iundisjfi  32770  algextdeglem6  33727  constrfin  33751  locfinreflem  33845  zarcls  33879  ordtconnlem1  33929  esumrnmpt2  34073  esumpinfval  34078  hasheuni  34090  ldsysgenld  34165  measvuni  34219  eulerpartlemn  34386  ballotlem7  34541  ballotth  34543  reprdifc  34632  bnj1230  34806  bnj1476  34851  bnj1204  35016  bnj1311  35028  onvf1odlem2  35140  satfv1  35399  bj-rabtrALT  36965  topdifinfindis  37380  icorempo  37385  isbasisrelowllem1  37389  isbasisrelowllem2  37390  relowlssretop  37397  phpreu  37644  poimirlem26  37686  poimirlem27  37687  mbfposadd  37707  cover2  37755  naddwordnexlem4  43434  rababg  43607  permaxsep  45040  rfcnpre1  45056  rfcnpre2  45068  ssrab2f  45154  infnsuprnmpt  45287  allbutfiinf  45458  supminfxr2  45507  pimxrneun  45526  limcperiod  45668  fnlimcnv  45705  fnlimfvre2  45715  fnlimf  45716  limsupequzmpt2  45756  liminfequzmpt2  45829  dvcosre  45950  stoweidlem14  46052  stoweidlem26  46064  stoweidlem31  46069  stoweidlem34  46072  stoweidlem35  46073  stoweidlem46  46084  stoweidlem50  46088  stoweidlem51  46089  stoweidlem52  46090  stoweidlem53  46091  stoweidlem54  46092  stoweidlem57  46095  stoweidlem59  46097  fourierdlem20  46165  fourierdlem31  46176  fourierdlem79  46223  sge0iunmptlemre  46453  ovnlerp  46600  opnvonmbllem1  46670  preimagelt  46737  preimalegt  46738  pimconstlt1  46740  pimltpnff  46741  pimrecltpos  46746  pimiooltgt  46748  pimdecfgtioc  46753  pimincfltioc  46754  pimdecfgtioo  46755  pimincfltioo  46756  preimageiingt  46758  preimaleiinlt  46759  pimgtmnff  46760  pimrecltneg  46762  sssmf  46776  incsmflem  46779  issmfle  46783  issmfgt  46794  smfaddlem1  46801  decsmflem  46804  issmfge  46808  smflimlem2  46810  smflim  46815  smfresal  46826  smfmullem2  46830  smfmullem4  46832  smfpimbor1lem2  46837  smflim2  46844  smfpimcclem  46845  smfsup  46852  smfinf  46856  smflimsuplem2  46859  smflimsuplem5  46862  smflimsuplem7  46864  smflimsup  46866  smfliminf  46869  smfdivdmmbl2  46879  fsupdm  46880  fsupdm2  46881  finfdm  46884  finfdm2  46885  prmdvdsfmtnof1lem1  47615