Theorem nfrab1 3440

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

Syntax hints:   ∧ wa 395   ∈ wcel 2107  {cab 2712  Ⅎwnfc 2882  {crab 3419

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-rab 3420

This theorem is referenced by:  rabss3d  4061  eqrrabd  4066  reusv2lem4  5381  reusv2  5383  rabxfrd  5397  fimarab  6963  riotaxfrd  7404  onminsb  7796  tfis  7858  oawordeulem  8574  nnawordex  8657  rankidb  9822  tskwe  9972  cardmin2  10021  cardaleph  10111  cardmin  10586  nnwos  12939  neiptopnei  23086  dissnlocfin  23483  imasnopn  23644  imasncld  23645  imasncls  23646  blval2  24519  iundisj  25519  mbfinf  25636  sltval2  27637  lfgrnloop  29070  difrab2  32445  rabexgfGS  32446  iundisjf  32537  aciunf1  32608  fpwrelmap  32679  fpwrelmapffs  32680  iundisjfi  32737  algextdeglem6  33702  constrfin  33726  locfinreflem  33798  zarcls  33832  ordtconnlem1  33882  esumrnmpt2  34028  esumpinfval  34033  hasheuni  34045  ldsysgenld  34120  measvuni  34174  eulerpartlemn  34342  ballotlem7  34497  ballotth  34499  reprdifc  34601  bnj1230  34775  bnj1476  34820  bnj1204  34985  bnj1311  34997  satfv1  35327  bj-rabtrALT  36891  topdifinfindis  37306  icorempo  37311  isbasisrelowllem1  37315  isbasisrelowllem2  37316  relowlssretop  37323  phpreu  37570  poimirlem26  37612  poimirlem27  37613  mbfposadd  37633  cover2  37681  naddwordnexlem4  43376  rababg  43549  rfcnpre1  44981  rfcnpre2  44993  ssrab2f  45079  infnsuprnmpt  45214  allbutfiinf  45388  supminfxr2  45437  pimxrneun  45456  limcperiod  45600  fnlimcnv  45639  fnlimfvre2  45649  fnlimf  45650  limsupequzmpt2  45690  liminfequzmpt2  45763  dvcosre  45884  stoweidlem14  45986  stoweidlem26  45998  stoweidlem31  46003  stoweidlem34  46006  stoweidlem35  46007  stoweidlem46  46018  stoweidlem50  46022  stoweidlem51  46023  stoweidlem52  46024  stoweidlem53  46025  stoweidlem54  46026  stoweidlem57  46029  stoweidlem59  46031  fourierdlem20  46099  fourierdlem31  46110  fourierdlem79  46157  sge0iunmptlemre  46387  ovnlerp  46534  opnvonmbllem1  46604  preimagelt  46671  preimalegt  46672  pimconstlt1  46674  pimltpnff  46675  pimrecltpos  46680  pimiooltgt  46682  pimdecfgtioc  46687  pimincfltioc  46688  pimdecfgtioo  46689  pimincfltioo  46690  preimageiingt  46692  preimaleiinlt  46693  pimgtmnff  46694  pimrecltneg  46696  sssmf  46710  incsmflem  46713  issmfle  46717  issmfgt  46728  smfaddlem1  46735  decsmflem  46738  issmfge  46742  smflimlem2  46744  smflim  46749  smfresal  46760  smfmullem2  46764  smfmullem4  46766  smfpimbor1lem2  46771  smflim2  46778  smfpimcclem  46779  smfsup  46786  smfinf  46790  smflimsuplem2  46793  smflimsuplem5  46796  smflimsuplem7  46798  smflimsup  46800  smfliminf  46803  smfdivdmmbl2  46813  fsupdm  46814  fsupdm2  46815  finfdm  46818  finfdm2  46819  prmdvdsfmtnof1lem1  47529