Theorem nfrab1 3421

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

Syntax hints:   ∧ wa 395   ∈ wcel 2114  {cab 2715  Ⅎwnfc 2884  {crab 3401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rab 3402

This theorem is referenced by:  rabss3d  4035  eqrrabd  4040  reusv2lem4  5348  reusv2  5350  rabxfrd  5364  fimarab  6916  riotaxfrd  7359  onminsb  7749  tfis  7807  oawordeulem  8491  nnawordex  8575  rankidb  9724  tskwe  9874  cardmin2  9923  cardaleph  10011  cardmin  10486  nnwos  12840  neiptopnei  23088  dissnlocfin  23485  imasnopn  23646  imasncld  23647  imasncls  23648  blval2  24518  iundisj  25517  mbfinf  25634  ltsval2  27636  lfgrnloop  29210  difrab2  32583  rabexgfGS  32585  iundisjf  32675  aciunf1  32752  fpwrelmap  32822  fpwrelmapffs  32823  iundisjfi  32886  algextdeglem6  33899  constrfin  33923  locfinreflem  34017  zarcls  34051  ordtconnlem1  34101  esumrnmpt2  34245  esumpinfval  34250  hasheuni  34262  ldsysgenld  34337  measvuni  34391  eulerpartlemn  34558  ballotlem7  34713  ballotth  34715  reprdifc  34804  bnj1230  34977  bnj1476  35022  bnj1204  35187  bnj1311  35199  onvf1odlem2  35317  satfv1  35576  bj-rabtrALT  37176  topdifinfindis  37598  icorempo  37603  isbasisrelowllem1  37607  isbasisrelowllem2  37608  relowlssretop  37615  phpreu  37852  poimirlem26  37894  poimirlem27  37895  mbfposadd  37915  cover2  37963  naddwordnexlem4  43755  rababg  43927  permaxsep  45360  rfcnpre1  45376  rfcnpre2  45388  ssrab2f  45473  infnsuprnmpt  45605  allbutfiinf  45775  supminfxr2  45824  pimxrneun  45843  limcperiod  45985  fnlimcnv  46022  fnlimfvre2  46032  fnlimf  46033  limsupequzmpt2  46073  liminfequzmpt2  46146  dvcosre  46267  stoweidlem14  46369  stoweidlem26  46381  stoweidlem31  46386  stoweidlem34  46389  stoweidlem35  46390  stoweidlem46  46401  stoweidlem50  46405  stoweidlem51  46406  stoweidlem52  46407  stoweidlem53  46408  stoweidlem54  46409  stoweidlem57  46412  stoweidlem59  46414  fourierdlem20  46482  fourierdlem31  46493  fourierdlem79  46540  sge0iunmptlemre  46770  ovnlerp  46917  opnvonmbllem1  46987  preimagelt  47054  preimalegt  47055  pimconstlt1  47057  pimltpnff  47058  pimrecltpos  47063  pimiooltgt  47065  pimdecfgtioc  47070  pimincfltioc  47071  pimdecfgtioo  47072  pimincfltioo  47073  preimageiingt  47075  preimaleiinlt  47076  pimgtmnff  47077  pimrecltneg  47079  sssmf  47093  incsmflem  47096  issmfle  47100  issmfgt  47111  smfaddlem1  47118  decsmflem  47121  issmfge  47125  smflimlem2  47127  smflim  47132  smfresal  47143  smfmullem2  47147  smfmullem4  47149  smfpimbor1lem2  47154  smflim2  47161  smfpimcclem  47162  smfsup  47169  smfinf  47173  smflimsuplem2  47176  smflimsuplem5  47179  smflimsuplem7  47181  smflimsup  47183  smfliminf  47186  smfdivdmmbl2  47196  fsupdm  47197  fsupdm2  47198  finfdm  47201  finfdm2  47202  prmdvdsfmtnof1lem1  47941