Theorem nfrab1 3416

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

Syntax hints:   ∧ wa 395   ∈ wcel 2113  {cab 2711  Ⅎwnfc 2880  {crab 3396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-rab 3397

This theorem is referenced by:  rabss3d  4030  eqrrabd  4035  reusv2lem4  5343  reusv2  5345  rabxfrd  5359  fimarab  6905  riotaxfrd  7346  onminsb  7736  tfis  7794  oawordeulem  8478  nnawordex  8561  rankidb  9704  tskwe  9854  cardmin2  9903  cardaleph  9991  cardmin  10466  nnwos  12819  neiptopnei  23067  dissnlocfin  23464  imasnopn  23625  imasncld  23626  imasncls  23627  blval2  24497  iundisj  25496  mbfinf  25613  sltval2  27615  lfgrnloop  29124  difrab2  32498  rabexgfGS  32500  iundisjf  32590  aciunf1  32667  fpwrelmap  32740  fpwrelmapffs  32741  iundisjfi  32804  algextdeglem6  33807  constrfin  33831  locfinreflem  33925  zarcls  33959  ordtconnlem1  34009  esumrnmpt2  34153  esumpinfval  34158  hasheuni  34170  ldsysgenld  34245  measvuni  34299  eulerpartlemn  34466  ballotlem7  34621  ballotth  34623  reprdifc  34712  bnj1230  34886  bnj1476  34931  bnj1204  35096  bnj1311  35108  onvf1odlem2  35220  satfv1  35479  bj-rabtrALT  37048  topdifinfindis  37463  icorempo  37468  isbasisrelowllem1  37472  isbasisrelowllem2  37473  relowlssretop  37480  phpreu  37717  poimirlem26  37759  poimirlem27  37760  mbfposadd  37780  cover2  37828  naddwordnexlem4  43558  rababg  43731  permaxsep  45164  rfcnpre1  45180  rfcnpre2  45192  ssrab2f  45277  infnsuprnmpt  45410  allbutfiinf  45580  supminfxr2  45629  pimxrneun  45648  limcperiod  45790  fnlimcnv  45827  fnlimfvre2  45837  fnlimf  45838  limsupequzmpt2  45878  liminfequzmpt2  45951  dvcosre  46072  stoweidlem14  46174  stoweidlem26  46186  stoweidlem31  46191  stoweidlem34  46194  stoweidlem35  46195  stoweidlem46  46206  stoweidlem50  46210  stoweidlem51  46211  stoweidlem52  46212  stoweidlem53  46213  stoweidlem54  46214  stoweidlem57  46217  stoweidlem59  46219  fourierdlem20  46287  fourierdlem31  46298  fourierdlem79  46345  sge0iunmptlemre  46575  ovnlerp  46722  opnvonmbllem1  46792  preimagelt  46859  preimalegt  46860  pimconstlt1  46862  pimltpnff  46863  pimrecltpos  46868  pimiooltgt  46870  pimdecfgtioc  46875  pimincfltioc  46876  pimdecfgtioo  46877  pimincfltioo  46878  preimageiingt  46880  preimaleiinlt  46881  pimgtmnff  46882  pimrecltneg  46884  sssmf  46898  incsmflem  46901  issmfle  46905  issmfgt  46916  smfaddlem1  46923  decsmflem  46926  issmfge  46930  smflimlem2  46932  smflim  46937  smfresal  46948  smfmullem2  46952  smfmullem4  46954  smfpimbor1lem2  46959  smflim2  46966  smfpimcclem  46967  smfsup  46974  smfinf  46978  smflimsuplem2  46981  smflimsuplem5  46984  smflimsuplem7  46986  smflimsup  46988  smfliminf  46991  smfdivdmmbl2  47001  fsupdm  47002  fsupdm2  47003  finfdm  47006  finfdm2  47007  prmdvdsfmtnof1lem1  47746