Theorem nfrab1 3439

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

Syntax hints:   ∧ wa 394   ∈ wcel 2099  {cab 2703  Ⅎwnfc 2876  {crab 3419

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-rab 3420

This theorem is referenced by:  rabss3d  4078  reusv2lem4  5407  reusv2  5409  rabxfrd  5423  riotaxfrd  7417  onminsb  7805  tfis  7867  oawordeulem  8586  nnawordex  8669  rankidb  9845  tskwe  9995  cardmin2  10044  cardaleph  10134  cardmin  10609  nnwos  12953  neiptopnei  23130  dissnlocfin  23527  imasnopn  23688  imasncld  23689  imasncls  23690  blval2  24565  iundisj  25571  mbfinf  25688  sltval2  27689  lfgrnloop  29064  difrab2  32429  rabexgfGS  32430  eqrrabd  32432  iundisjf  32511  fimarab  32562  aciunf1  32582  fpwrelmap  32649  fpwrelmapffs  32650  iundisjfi  32700  algextdeglem6  33591  locfinreflem  33657  zarcls  33691  ordtconnlem1  33741  esumrnmpt2  33903  esumpinfval  33908  hasheuni  33920  ldsysgenld  33995  measvuni  34049  eulerpartlemn  34217  ballotlem7  34371  ballotth  34373  reprdifc  34475  bnj1230  34649  bnj1476  34694  bnj1204  34859  bnj1311  34871  satfv1  35193  bj-rabtrALT  36639  topdifinfindis  37055  icorempo  37060  isbasisrelowllem1  37064  isbasisrelowllem2  37065  relowlssretop  37072  phpreu  37307  poimirlem26  37349  poimirlem27  37350  mbfposadd  37370  cover2  37418  naddwordnexlem4  43086  rababg  43259  rfcnpre1  44636  rfcnpre2  44648  ssrab2f  44736  infnsuprnmpt  44877  allbutfiinf  45053  supminfxr2  45102  pimxrneun  45122  fsumiunss  45214  limcperiod  45267  fnlimcnv  45306  fnlimfvre2  45316  fnlimf  45317  limsupequzmpt2  45357  liminfequzmpt2  45430  dvcosre  45551  stoweidlem14  45653  stoweidlem26  45665  stoweidlem31  45670  stoweidlem34  45673  stoweidlem35  45674  stoweidlem46  45685  stoweidlem50  45689  stoweidlem51  45690  stoweidlem52  45691  stoweidlem53  45692  stoweidlem54  45693  stoweidlem57  45696  stoweidlem59  45698  fourierdlem20  45766  fourierdlem31  45777  fourierdlem79  45824  sge0iunmptlemre  46054  ovnlerp  46201  opnvonmbllem1  46271  preimagelt  46338  preimalegt  46339  pimconstlt1  46341  pimltpnff  46342  pimrecltpos  46347  pimiooltgt  46349  pimdecfgtioc  46354  pimincfltioc  46355  pimdecfgtioo  46356  pimincfltioo  46357  preimageiingt  46359  preimaleiinlt  46360  pimgtmnff  46361  pimrecltneg  46363  sssmf  46377  incsmflem  46380  issmfle  46384  issmfgt  46395  smfaddlem1  46402  decsmflem  46405  issmfge  46409  smflimlem2  46411  smflim  46416  smfresal  46427  smfmullem2  46431  smfmullem4  46433  smfpimbor1lem2  46438  smflim2  46445  smfpimcclem  46446  smfsup  46453  smfinf  46457  smflimsuplem2  46460  smflimsuplem5  46463  smflimsuplem7  46465  smflimsup  46467  smfliminf  46470  smfdivdmmbl2  46480  fsupdm  46481  fsupdm2  46482  finfdm  46485  finfdm2  46486  prmdvdsfmtnof1lem1  47174