Theorem nfrab1 3436

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

Syntax hints:   ∧ wa 395   ∈ wcel 2108  {cab 2713  Ⅎwnfc 2883  {crab 3415

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-rab 3416

This theorem is referenced by:  rabss3d  4056  eqrrabd  4061  reusv2lem4  5371  reusv2  5373  rabxfrd  5387  fimarab  6952  riotaxfrd  7394  onminsb  7786  tfis  7848  oawordeulem  8564  nnawordex  8647  rankidb  9812  tskwe  9962  cardmin2  10011  cardaleph  10101  cardmin  10576  nnwos  12929  neiptopnei  23068  dissnlocfin  23465  imasnopn  23626  imasncld  23627  imasncls  23628  blval2  24499  iundisj  25499  mbfinf  25616  sltval2  27618  lfgrnloop  29050  difrab2  32425  rabexgfGS  32426  iundisjf  32516  aciunf1  32587  fpwrelmap  32656  fpwrelmapffs  32657  iundisjfi  32719  algextdeglem6  33702  constrfin  33726  locfinreflem  33817  zarcls  33851  ordtconnlem1  33901  esumrnmpt2  34045  esumpinfval  34050  hasheuni  34062  ldsysgenld  34137  measvuni  34191  eulerpartlemn  34359  ballotlem7  34514  ballotth  34516  reprdifc  34605  bnj1230  34779  bnj1476  34824  bnj1204  34989  bnj1311  35001  satfv1  35331  bj-rabtrALT  36895  topdifinfindis  37310  icorempo  37315  isbasisrelowllem1  37319  isbasisrelowllem2  37320  relowlssretop  37327  phpreu  37574  poimirlem26  37616  poimirlem27  37617  mbfposadd  37637  cover2  37685  naddwordnexlem4  43372  rababg  43545  permaxsep  44980  rfcnpre1  44991  rfcnpre2  45003  ssrab2f  45089  infnsuprnmpt  45222  allbutfiinf  45395  supminfxr2  45444  pimxrneun  45463  limcperiod  45605  fnlimcnv  45644  fnlimfvre2  45654  fnlimf  45655  limsupequzmpt2  45695  liminfequzmpt2  45768  dvcosre  45889  stoweidlem14  45991  stoweidlem26  46003  stoweidlem31  46008  stoweidlem34  46011  stoweidlem35  46012  stoweidlem46  46023  stoweidlem50  46027  stoweidlem51  46028  stoweidlem52  46029  stoweidlem53  46030  stoweidlem54  46031  stoweidlem57  46034  stoweidlem59  46036  fourierdlem20  46104  fourierdlem31  46115  fourierdlem79  46162  sge0iunmptlemre  46392  ovnlerp  46539  opnvonmbllem1  46609  preimagelt  46676  preimalegt  46677  pimconstlt1  46679  pimltpnff  46680  pimrecltpos  46685  pimiooltgt  46687  pimdecfgtioc  46692  pimincfltioc  46693  pimdecfgtioo  46694  pimincfltioo  46695  preimageiingt  46697  preimaleiinlt  46698  pimgtmnff  46699  pimrecltneg  46701  sssmf  46715  incsmflem  46718  issmfle  46722  issmfgt  46733  smfaddlem1  46740  decsmflem  46743  issmfge  46747  smflimlem2  46749  smflim  46754  smfresal  46765  smfmullem2  46769  smfmullem4  46771  smfpimbor1lem2  46776  smflim2  46783  smfpimcclem  46784  smfsup  46791  smfinf  46795  smflimsuplem2  46798  smflimsuplem5  46801  smflimsuplem7  46803  smflimsup  46805  smfliminf  46808  smfdivdmmbl2  46818  fsupdm  46819  fsupdm2  46820  finfdm  46823  finfdm2  46824  prmdvdsfmtnof1lem1  47546