Theorem nfrab1 3429

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

Syntax hints:   ∧ wa 395   ∈ wcel 2109  {cab 2708  Ⅎwnfc 2877  {crab 3408

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-rab 3409

This theorem is referenced by:  rabss3d  4047  eqrrabd  4052  reusv2lem4  5359  reusv2  5361  rabxfrd  5375  fimarab  6938  riotaxfrd  7381  onminsb  7773  tfis  7834  oawordeulem  8521  nnawordex  8604  rankidb  9760  tskwe  9910  cardmin2  9959  cardaleph  10049  cardmin  10524  nnwos  12881  neiptopnei  23026  dissnlocfin  23423  imasnopn  23584  imasncld  23585  imasncls  23586  blval2  24457  iundisj  25456  mbfinf  25573  sltval2  27575  lfgrnloop  29059  difrab2  32434  rabexgfGS  32435  iundisjf  32525  aciunf1  32594  fpwrelmap  32663  fpwrelmapffs  32664  iundisjfi  32726  algextdeglem6  33719  constrfin  33743  locfinreflem  33837  zarcls  33871  ordtconnlem1  33921  esumrnmpt2  34065  esumpinfval  34070  hasheuni  34082  ldsysgenld  34157  measvuni  34211  eulerpartlemn  34379  ballotlem7  34534  ballotth  34536  reprdifc  34625  bnj1230  34799  bnj1476  34844  bnj1204  35009  bnj1311  35021  onvf1odlem2  35098  satfv1  35357  bj-rabtrALT  36926  topdifinfindis  37341  icorempo  37346  isbasisrelowllem1  37350  isbasisrelowllem2  37351  relowlssretop  37358  phpreu  37605  poimirlem26  37647  poimirlem27  37648  mbfposadd  37668  cover2  37716  naddwordnexlem4  43397  rababg  43570  permaxsep  45004  rfcnpre1  45020  rfcnpre2  45032  ssrab2f  45118  infnsuprnmpt  45251  allbutfiinf  45423  supminfxr2  45472  pimxrneun  45491  limcperiod  45633  fnlimcnv  45672  fnlimfvre2  45682  fnlimf  45683  limsupequzmpt2  45723  liminfequzmpt2  45796  dvcosre  45917  stoweidlem14  46019  stoweidlem26  46031  stoweidlem31  46036  stoweidlem34  46039  stoweidlem35  46040  stoweidlem46  46051  stoweidlem50  46055  stoweidlem51  46056  stoweidlem52  46057  stoweidlem53  46058  stoweidlem54  46059  stoweidlem57  46062  stoweidlem59  46064  fourierdlem20  46132  fourierdlem31  46143  fourierdlem79  46190  sge0iunmptlemre  46420  ovnlerp  46567  opnvonmbllem1  46637  preimagelt  46704  preimalegt  46705  pimconstlt1  46707  pimltpnff  46708  pimrecltpos  46713  pimiooltgt  46715  pimdecfgtioc  46720  pimincfltioc  46721  pimdecfgtioo  46722  pimincfltioo  46723  preimageiingt  46725  preimaleiinlt  46726  pimgtmnff  46727  pimrecltneg  46729  sssmf  46743  incsmflem  46746  issmfle  46750  issmfgt  46761  smfaddlem1  46768  decsmflem  46771  issmfge  46775  smflimlem2  46777  smflim  46782  smfresal  46793  smfmullem2  46797  smfmullem4  46799  smfpimbor1lem2  46804  smflim2  46811  smfpimcclem  46812  smfsup  46819  smfinf  46823  smflimsuplem2  46826  smflimsuplem5  46829  smflimsuplem7  46831  smflimsup  46833  smfliminf  46836  smfdivdmmbl2  46846  fsupdm  46847  fsupdm2  46848  finfdm  46851  finfdm2  46852  prmdvdsfmtnof1lem1  47589