Theorem nfrab1 3417

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

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

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 3397

This theorem is referenced by:  rabss3d  4034  eqrrabd  4039  reusv2lem4  5343  reusv2  5345  rabxfrd  5359  fimarab  6901  riotaxfrd  7344  onminsb  7734  tfis  7795  oawordeulem  8479  nnawordex  8562  rankidb  9715  tskwe  9865  cardmin2  9914  cardaleph  10002  cardmin  10477  nnwos  12834  neiptopnei  23035  dissnlocfin  23432  imasnopn  23593  imasncld  23594  imasncls  23595  blval2  24466  iundisj  25465  mbfinf  25582  sltval2  27584  lfgrnloop  29088  difrab2  32460  rabexgfGS  32461  iundisjf  32551  aciunf1  32620  fpwrelmap  32689  fpwrelmapffs  32690  iundisjfi  32752  algextdeglem6  33691  constrfin  33715  locfinreflem  33809  zarcls  33843  ordtconnlem1  33893  esumrnmpt2  34037  esumpinfval  34042  hasheuni  34054  ldsysgenld  34129  measvuni  34183  eulerpartlemn  34351  ballotlem7  34506  ballotth  34508  reprdifc  34597  bnj1230  34771  bnj1476  34816  bnj1204  34981  bnj1311  34993  onvf1odlem2  35079  satfv1  35338  bj-rabtrALT  36907  topdifinfindis  37322  icorempo  37327  isbasisrelowllem1  37331  isbasisrelowllem2  37332  relowlssretop  37339  phpreu  37586  poimirlem26  37628  poimirlem27  37629  mbfposadd  37649  cover2  37697  naddwordnexlem4  43377  rababg  43550  permaxsep  44984  rfcnpre1  45000  rfcnpre2  45012  ssrab2f  45098  infnsuprnmpt  45231  allbutfiinf  45403  supminfxr2  45452  pimxrneun  45471  limcperiod  45613  fnlimcnv  45652  fnlimfvre2  45662  fnlimf  45663  limsupequzmpt2  45703  liminfequzmpt2  45776  dvcosre  45897  stoweidlem14  45999  stoweidlem26  46011  stoweidlem31  46016  stoweidlem34  46019  stoweidlem35  46020  stoweidlem46  46031  stoweidlem50  46035  stoweidlem51  46036  stoweidlem52  46037  stoweidlem53  46038  stoweidlem54  46039  stoweidlem57  46042  stoweidlem59  46044  fourierdlem20  46112  fourierdlem31  46123  fourierdlem79  46170  sge0iunmptlemre  46400  ovnlerp  46547  opnvonmbllem1  46617  preimagelt  46684  preimalegt  46685  pimconstlt1  46687  pimltpnff  46688  pimrecltpos  46693  pimiooltgt  46695  pimdecfgtioc  46700  pimincfltioc  46701  pimdecfgtioo  46702  pimincfltioo  46703  preimageiingt  46705  preimaleiinlt  46706  pimgtmnff  46707  pimrecltneg  46709  sssmf  46723  incsmflem  46726  issmfle  46730  issmfgt  46741  smfaddlem1  46748  decsmflem  46751  issmfge  46755  smflimlem2  46757  smflim  46762  smfresal  46773  smfmullem2  46777  smfmullem4  46779  smfpimbor1lem2  46784  smflim2  46791  smfpimcclem  46792  smfsup  46799  smfinf  46803  smflimsuplem2  46806  smflimsuplem5  46809  smflimsuplem7  46811  smflimsup  46813  smfliminf  46816  smfdivdmmbl2  46826  fsupdm  46827  fsupdm2  46828  finfdm  46831  finfdm2  46832  prmdvdsfmtnof1lem1  47572