Theorem nfrab1 3426

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

Syntax hints:   ∧ wa 395   ∈ wcel 2109  {cab 2707  Ⅎwnfc 2876  {crab 3405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3406

This theorem is referenced by:  rabss3d  4044  eqrrabd  4049  reusv2lem4  5356  reusv2  5358  rabxfrd  5372  fimarab  6935  riotaxfrd  7378  onminsb  7770  tfis  7831  oawordeulem  8518  nnawordex  8601  rankidb  9753  tskwe  9903  cardmin2  9952  cardaleph  10042  cardmin  10517  nnwos  12874  neiptopnei  23019  dissnlocfin  23416  imasnopn  23577  imasncld  23578  imasncls  23579  blval2  24450  iundisj  25449  mbfinf  25566  sltval2  27568  lfgrnloop  29052  difrab2  32427  rabexgfGS  32428  iundisjf  32518  aciunf1  32587  fpwrelmap  32656  fpwrelmapffs  32657  iundisjfi  32719  algextdeglem6  33712  constrfin  33736  locfinreflem  33830  zarcls  33864  ordtconnlem1  33914  esumrnmpt2  34058  esumpinfval  34063  hasheuni  34075  ldsysgenld  34150  measvuni  34204  eulerpartlemn  34372  ballotlem7  34527  ballotth  34529  reprdifc  34618  bnj1230  34792  bnj1476  34837  bnj1204  35002  bnj1311  35014  onvf1odlem2  35091  satfv1  35350  bj-rabtrALT  36919  topdifinfindis  37334  icorempo  37339  isbasisrelowllem1  37343  isbasisrelowllem2  37344  relowlssretop  37351  phpreu  37598  poimirlem26  37640  poimirlem27  37641  mbfposadd  37661  cover2  37709  naddwordnexlem4  43390  rababg  43563  permaxsep  44997  rfcnpre1  45013  rfcnpre2  45025  ssrab2f  45111  infnsuprnmpt  45244  allbutfiinf  45416  supminfxr2  45465  pimxrneun  45484  limcperiod  45626  fnlimcnv  45665  fnlimfvre2  45675  fnlimf  45676  limsupequzmpt2  45716  liminfequzmpt2  45789  dvcosre  45910  stoweidlem14  46012  stoweidlem26  46024  stoweidlem31  46029  stoweidlem34  46032  stoweidlem35  46033  stoweidlem46  46044  stoweidlem50  46048  stoweidlem51  46049  stoweidlem52  46050  stoweidlem53  46051  stoweidlem54  46052  stoweidlem57  46055  stoweidlem59  46057  fourierdlem20  46125  fourierdlem31  46136  fourierdlem79  46183  sge0iunmptlemre  46413  ovnlerp  46560  opnvonmbllem1  46630  preimagelt  46697  preimalegt  46698  pimconstlt1  46700  pimltpnff  46701  pimrecltpos  46706  pimiooltgt  46708  pimdecfgtioc  46713  pimincfltioc  46714  pimdecfgtioo  46715  pimincfltioo  46716  preimageiingt  46718  preimaleiinlt  46719  pimgtmnff  46720  pimrecltneg  46722  sssmf  46736  incsmflem  46739  issmfle  46743  issmfgt  46754  smfaddlem1  46761  decsmflem  46764  issmfge  46768  smflimlem2  46770  smflim  46775  smfresal  46786  smfmullem2  46790  smfmullem4  46792  smfpimbor1lem2  46797  smflim2  46804  smfpimcclem  46805  smfsup  46812  smfinf  46816  smflimsuplem2  46819  smflimsuplem5  46822  smflimsuplem7  46824  smflimsup  46826  smfliminf  46829  smfdivdmmbl2  46839  fsupdm  46840  fsupdm2  46841  finfdm  46844  finfdm2  46845  prmdvdsfmtnof1lem1  47585