Theorem nfrab1 3309

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

Syntax hints:   ∧ wa 386   ∈ wcel 2107  {cab 2763  Ⅎwnfc 2919  {crab 3094

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099

This theorem is referenced by:  rabrabi  3397  reusv2lem4  5115  reusv2  5117  rabxfrd  5131  riotaxfrd  6916  onminsb  7279  tfis  7334  oawordeulem  7920  nnawordex  8003  rankidb  8962  tskwe  9111  cardmin2  9159  cardaleph  9247  cardmin  9723  nnwos  12067  neiptopnei  21355  dissnlocfin  21752  imasnopn  21913  imasncld  21914  imasncls  21915  blval2  22786  iundisj  23763  mbfinf  23880  lfgrnloop  26490  extwwlkfab  27782  extwwlkfabOLD  27783  numclwwlk1lem2OLDOLD  27800  difrab2  29918  rabexgfGS  29919  rabss3d  29930  iundisjf  29982  fimarab  30027  aciunf1  30045  fpwrelmap  30091  fpwrelmapffs  30092  iundisjfi  30133  locfinreflem  30513  ordtconnlem1  30576  esumrnmpt2  30736  esumpinfval  30741  hasheuni  30753  ldsysgenld  30829  measvuni  30883  eulerpartlemn  31049  ballotlem7  31204  ballotth  31206  reprdifc  31315  bnj1230  31480  bnj1476  31524  bnj1204  31687  bnj1311  31699  sltval2  32406  bj-rabtrALT  33509  topdifinfindis  33796  icorempt2  33801  isbasisrelowllem1  33805  isbasisrelowllem2  33806  relowlssretop  33813  phpreu  34027  poimirlem26  34070  poimirlem27  34071  mbfposadd  34091  cover2  34142  rababg  38850  rfcnpre1  40125  rfcnpre2  40137  ssrab2f  40243  infnsuprnmpt  40390  allbutfiinf  40567  supminfxr2  40618  fsumiunss  40729  limcperiod  40782  fnlimcnv  40821  fnlimfvre2  40831  fnlimf  40832  limsupequzmpt2  40872  liminfequzmpt2  40945  dvcosre  41068  stoweidlem14  41172  stoweidlem26  41184  stoweidlem31  41189  stoweidlem34  41192  stoweidlem35  41193  stoweidlem46  41204  stoweidlem50  41208  stoweidlem51  41209  stoweidlem52  41210  stoweidlem53  41211  stoweidlem54  41212  stoweidlem57  41215  stoweidlem59  41217  fourierdlem20  41285  fourierdlem31  41296  fourierdlem79  41343  sge0iunmptlemre  41570  ovnlerp  41717  opnvonmbllem1  41787  preimagelt  41853  preimalegt  41854  pimconstlt1  41856  pimltpnf  41857  pimrecltpos  41860  pimiooltgt  41862  pimdecfgtioc  41866  pimincfltioc  41867  pimdecfgtioo  41868  pimincfltioo  41869  preimageiingt  41871  preimaleiinlt  41872  pimrecltneg  41874  sssmf  41888  incsmflem  41891  issmfle  41895  issmfgt  41906  smfaddlem1  41912  decsmflem  41915  issmfge  41919  smflimlem2  41921  smflim  41926  smfresal  41936  smfmullem2  41940  smfmullem4  41942  smfpimbor1lem2  41947  smflim2  41953  smfpimcclem  41954  smfsup  41961  smfinf  41965  smflimsuplem2  41968  smflimsuplem5  41971  smflimsuplem7  41973  smflimsup  41975  smfliminf  41978  prmdvdsfmtnof1lem1  42531