Theorem nfrab1 3411

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

Syntax hints:   ∧ wa 396   ∈ wcel 2119  {cab 2717  Ⅎwnfc 2886  {crab 3391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-rab 3392

This theorem is referenced by:  rabss3d  4012  eqrrabd  4017  reusv2lem4  5330  reusv2  5332  rabxfrd  5346  fimarab  6901  riotaxfrd  7347  onminsb  7737  tfis  7795  oawordeulem  8479  nnawordex  8563  rankidb  9715  tskwe  9865  cardmin2  9914  cardaleph  10002  cardmin  10477  nnwos  12856  neiptopnei  23115  dissnlocfin  23512  imasnopn  23673  imasncld  23674  imasncls  23675  blval2  24545  iundisj  25533  mbfinf  25650  ltsval2  27638  lfgrnloop  29212  difrab2  32585  rabexgfGS  32587  iundisjf  32678  aciunf1  32755  fpwrelmap  32825  fpwrelmapffs  32826  iundisjfi  32888  algextdeglem6  33906  constrfin  33930  locfinreflem  34024  zarcls  34058  ordtconnlem1  34108  esumrnmpt2  34252  esumpinfval  34257  hasheuni  34269  ldsysgenld  34344  measvuni  34398  eulerpartlemn  34565  ballotlem7  34720  ballotth  34722  reprdifc  34811  bnj1230  34984  bnj1476  35029  bnj1204  35194  bnj1311  35206  onvf1odlem2  35332  satfv1  35591  bj-rabtrALT  37284  topdifinfindis  37708  icorempo  37713  isbasisrelowllem1  37717  isbasisrelowllem2  37718  relowlssretop  37725  phpreu  37971  poimirlem26  38013  poimirlem27  38014  mbfposadd  38034  cover2  38082  naddwordnexlem4  43846  rababg  44018  permaxsep  45451  rfcnpre1  45467  rfcnpre2  45479  ssrab2f  45564  infnsuprnmpt  45694  allbutfiinf  45863  supminfxr2  45912  pimxrneun  45931  limcperiod  46073  fnlimcnv  46110  fnlimfvre2  46120  fnlimf  46121  limsupequzmpt2  46161  liminfequzmpt2  46234  dvcosre  46355  stoweidlem14  46457  stoweidlem26  46469  stoweidlem31  46474  stoweidlem34  46477  stoweidlem35  46478  stoweidlem46  46489  stoweidlem50  46493  stoweidlem51  46494  stoweidlem52  46495  stoweidlem53  46496  stoweidlem54  46497  stoweidlem57  46500  stoweidlem59  46502  fourierdlem20  46570  fourierdlem31  46581  fourierdlem79  46628  sge0iunmptlemre  46858  ovnlerp  47005  opnvonmbllem1  47075  preimagelt  47142  preimalegt  47143  pimconstlt1  47145  pimltpnff  47146  pimrecltpos  47151  pimiooltgt  47153  pimdecfgtioc  47158  pimincfltioc  47159  pimdecfgtioo  47160  pimincfltioo  47161  preimageiingt  47163  preimaleiinlt  47164  pimgtmnff  47165  pimrecltneg  47167  sssmf  47181  incsmflem  47184  issmfle  47188  issmfgt  47199  smfaddlem1  47206  decsmflem  47209  issmfge  47213  smflimlem2  47215  smflim  47220  smfresal  47231  smfmullem2  47235  smfmullem4  47237  smfpimbor1lem2  47242  smflim2  47249  smfpimcclem  47250  smfsup  47257  smfinf  47261  smflimsuplem2  47264  smflimsuplem5  47267  smflimsuplem7  47269  smflimsup  47271  smfliminf  47274  smfdivdmmbl2  47284  fsupdm  47285  fsupdm2  47286  finfdm  47289  finfdm2  47290  prmdvdsfmtnof1lem1  48062