Theorem nfrab1 3422

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

Syntax hints:   ∧ wa 396   ∈ wcel 2105  {cab 2713  Ⅎwnfc 2884  {crab 3403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-rab 3404

This theorem is referenced by:  reusv2lem4  5341  reusv2  5343  rabxfrd  5357  riotaxfrd  7321  onminsb  7699  tfis  7761  oawordeulem  8448  nnawordex  8531  rankidb  9649  tskwe  9799  cardmin2  9848  cardaleph  9938  cardmin  10413  nnwos  12748  neiptopnei  22381  dissnlocfin  22778  imasnopn  22939  imasncld  22940  imasncls  22941  blval2  23816  iundisj  24810  mbfinf  24927  sltval2  26902  lfgrnloop  27697  difrab2  31046  rabexgfGS  31047  eqrrabd  31050  rabss3d  31062  iundisjf  31128  fimarab  31180  aciunf1  31200  fpwrelmap  31268  fpwrelmapffs  31269  iundisjfi  31317  locfinreflem  32001  zarcls  32035  ordtconnlem1  32085  esumrnmpt2  32247  esumpinfval  32252  hasheuni  32264  ldsysgenld  32339  measvuni  32393  eulerpartlemn  32561  ballotlem7  32715  ballotth  32717  reprdifc  32820  bnj1230  32994  bnj1476  33039  bnj1204  33204  bnj1311  33216  satfv1  33537  bj-rabtrALT  35209  topdifinfindis  35615  icorempo  35620  isbasisrelowllem1  35624  isbasisrelowllem2  35625  relowlssretop  35632  phpreu  35859  poimirlem26  35901  poimirlem27  35902  mbfposadd  35922  cover2  35970  rababg  41491  rfcnpre1  42872  rfcnpre2  42884  ssrab2f  42976  infnsuprnmpt  43113  allbutfiinf  43284  supminfxr2  43333  pimxrneun  43353  fsumiunss  43441  limcperiod  43494  fnlimcnv  43533  fnlimfvre2  43543  fnlimf  43544  limsupequzmpt2  43584  liminfequzmpt2  43657  dvcosre  43778  stoweidlem14  43880  stoweidlem26  43892  stoweidlem31  43897  stoweidlem34  43900  stoweidlem35  43901  stoweidlem46  43912  stoweidlem50  43916  stoweidlem51  43917  stoweidlem52  43918  stoweidlem53  43919  stoweidlem54  43920  stoweidlem57  43923  stoweidlem59  43925  fourierdlem20  43993  fourierdlem31  44004  fourierdlem79  44051  sge0iunmptlemre  44279  ovnlerp  44426  opnvonmbllem1  44496  preimagelt  44563  preimalegt  44564  pimconstlt1  44566  pimltpnff  44567  pimrecltpos  44572  pimiooltgt  44574  pimdecfgtioc  44579  pimincfltioc  44580  pimdecfgtioo  44581  pimincfltioo  44582  preimageiingt  44584  preimaleiinlt  44585  pimgtmnff  44586  pimrecltneg  44588  sssmf  44602  incsmflem  44605  issmfle  44609  issmfgt  44620  smfaddlem1  44627  decsmflem  44630  issmfge  44634  smflimlem2  44636  smflim  44641  smfresal  44652  smfmullem2  44656  smfmullem4  44658  smfpimbor1lem2  44663  smflim2  44670  smfpimcclem  44671  smfsup  44678  smfinf  44682  smflimsuplem2  44685  smflimsuplem5  44688  smflimsuplem7  44690  smflimsup  44692  smfliminf  44695  smfdivdmmbl2  44705  prmdvdsfmtnof1lem1  45376