Theorem nfrab1 3099

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

Syntax hints:   ∧ wa 383   ∈ wcel 1977  {cab 2596  Ⅎwnfc 2738  {crab 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905

This theorem is referenced by:  reusv2lem4  4798  reusv2  4800  rabxfrd  4815  riotaxfrd  6541  onminsb  6891  tfis  6946  oawordeulem  7521  nnawordex  7604  rankidb  8546  tskwe  8659  cardmin2  8707  cardaleph  8795  cardmin  9265  nnwos  11631  neiptopnei  20746  dissnlocfin  21142  imasnopn  21303  imasncld  21304  imasncls  21305  blval2  22177  iundisj  23123  mbfinf  23238  lfgrnloop  25791  rabexgfGS  28725  rabss3d  28736  iundisjf  28784  fimarab  28825  aciunf1  28845  fpwrelmap  28896  fpwrelmapffs  28897  iundisjfi  28942  locfinreflem  29235  ordtconlem1  29298  esumrnmpt2  29457  esumpinfval  29462  hasheuni  29474  ldsysgenld  29550  measvuni  29604  eulerpartlemn  29770  ballotlem7  29924  ballotth  29926  bnj1230  30127  bnj1476  30171  bnj1204  30334  bnj1311  30346  sltval2  31053  nobndlem5  31095  bj-rabtrALT  32119  topdifinfindis  32370  icorempt2  32375  isbasisrelowllem1  32379  isbasisrelowllem2  32380  relowlssretop  32387  phpreu  32563  poimirlem26  32605  poimirlem27  32606  mbfposadd  32627  cover2  32678  rababg  36898  rfcnpre1  38201  rfcnpre2  38213  ssrab2f  38331  fsumiunss  38642  limcperiod  38695  fnlimcnv  38734  fnlimfvre2  38744  fnlimf  38745  dvcosre  38799  stoweidlem14  38907  stoweidlem26  38919  stoweidlem31  38924  stoweidlem34  38927  stoweidlem35  38928  stoweidlem46  38939  stoweidlem50  38943  stoweidlem51  38944  stoweidlem52  38945  stoweidlem53  38946  stoweidlem54  38947  stoweidlem57  38950  stoweidlem59  38952  fourierdlem20  39020  fourierdlem31  39031  fourierdlem79  39078  sge0iunmptlemre  39308  ovnlerp  39452  opnvonmbllem1  39522  preimagelt  39589  preimalegt  39590  pimconstlt1  39592  pimltpnf  39593  pimrecltpos  39596  pimiooltgt  39598  pimdecfgtioc  39602  pimincfltioc  39603  pimdecfgtioo  39604  pimincfltioo  39605  preimageiingt  39607  preimaleiinlt  39608  pimrecltneg  39610  sssmf  39625  incsmflem  39628  issmfle  39632  issmfgt  39643  smfaddlem1  39649  decsmflem  39652  issmfge  39656  smflimlem2  39658  smflim  39663  smfresal  39673  smfmullem2  39677  smfmullem4  39679  smfpimbor1lem2  39684  prmdvdsfmtnof1lem1  40034