Theorem nfrab1 3310

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

Syntax hints:   ∧ wa 395   ∈ wcel 2108  {cab 2715  Ⅎwnfc 2886  {crab 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-rab 3072

This theorem is referenced by:  reusv2lem4  5319  reusv2  5321  rabxfrd  5335  riotaxfrd  7247  onminsb  7621  tfis  7676  oawordeulem  8347  nnawordex  8430  rankidb  9489  tskwe  9639  cardmin2  9688  cardaleph  9776  cardmin  10251  nnwos  12584  neiptopnei  22191  dissnlocfin  22588  imasnopn  22749  imasncld  22750  imasncls  22751  blval2  23624  iundisj  24617  mbfinf  24734  lfgrnloop  27398  difrab2  30746  rabexgfGS  30747  eqrrabd  30750  rabss3d  30762  iundisjf  30829  fimarab  30881  aciunf1  30902  fpwrelmap  30970  fpwrelmapffs  30971  iundisjfi  31019  locfinreflem  31692  zarcls  31726  ordtconnlem1  31776  esumrnmpt2  31936  esumpinfval  31941  hasheuni  31953  ldsysgenld  32028  measvuni  32082  eulerpartlemn  32248  ballotlem7  32402  ballotth  32404  reprdifc  32507  bnj1230  32682  bnj1476  32727  bnj1204  32892  bnj1311  32904  satfv1  33225  sltval2  33786  bj-rabtrALT  35046  topdifinfindis  35444  icorempo  35449  isbasisrelowllem1  35453  isbasisrelowllem2  35454  relowlssretop  35461  phpreu  35688  poimirlem26  35730  poimirlem27  35731  mbfposadd  35751  cover2  35799  rababg  41070  rfcnpre1  42451  rfcnpre2  42463  ssrab2f  42555  infnsuprnmpt  42685  allbutfiinf  42850  supminfxr2  42899  fsumiunss  43006  limcperiod  43059  fnlimcnv  43098  fnlimfvre2  43108  fnlimf  43109  limsupequzmpt2  43149  liminfequzmpt2  43222  dvcosre  43343  stoweidlem14  43445  stoweidlem26  43457  stoweidlem31  43462  stoweidlem34  43465  stoweidlem35  43466  stoweidlem46  43477  stoweidlem50  43481  stoweidlem51  43482  stoweidlem52  43483  stoweidlem53  43484  stoweidlem54  43485  stoweidlem57  43488  stoweidlem59  43490  fourierdlem20  43558  fourierdlem31  43569  fourierdlem79  43616  sge0iunmptlemre  43843  ovnlerp  43990  opnvonmbllem1  44060  preimagelt  44126  preimalegt  44127  pimconstlt1  44129  pimltpnf  44130  pimrecltpos  44133  pimiooltgt  44135  pimdecfgtioc  44139  pimincfltioc  44140  pimdecfgtioo  44141  pimincfltioo  44142  preimageiingt  44144  preimaleiinlt  44145  pimrecltneg  44147  sssmf  44161  incsmflem  44164  issmfle  44168  issmfgt  44179  smfaddlem1  44185  decsmflem  44188  issmfge  44192  smflimlem2  44194  smflim  44199  smfresal  44209  smfmullem2  44213  smfmullem4  44215  smfpimbor1lem2  44220  smflim2  44226  smfpimcclem  44227  smfsup  44234  smfinf  44238  smflimsuplem2  44241  smflimsuplem5  44244  smflimsuplem7  44246  smflimsup  44248  smfliminf  44251  prmdvdsfmtnof1lem1  44924