Theorem nfrab1 3309

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

Syntax hints:   ∧ wa 386   ∈ wcel 2107  {cab 2763  Ⅎwnfc 2919  {crab 3094

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099

This theorem is referenced by:  rabrabi  3397  reusv2lem4  5113  reusv2  5115  rabxfrd  5129  riotaxfrd  6914  onminsb  7277  tfis  7332  oawordeulem  7918  nnawordex  8001  rankidb  8960  tskwe  9109  cardmin2  9157  cardaleph  9245  cardmin  9721  nnwos  12062  neiptopnei  21344  dissnlocfin  21741  imasnopn  21902  imasncld  21903  imasncls  21904  blval2  22775  iundisj  23752  mbfinf  23869  lfgrnloop  26473  extwwlkfab  27765  extwwlkfabOLD  27766  numclwwlk1lem2OLDOLD  27783  difrab2  29901  rabexgfGS  29902  rabss3d  29913  iundisjf  29965  fimarab  30010  aciunf1  30028  fpwrelmap  30074  fpwrelmapffs  30075  iundisjfi  30119  locfinreflem  30505  ordtconnlem1  30568  esumrnmpt2  30728  esumpinfval  30733  hasheuni  30745  ldsysgenld  30821  measvuni  30875  eulerpartlemn  31041  ballotlem7  31196  ballotth  31198  reprdifc  31307  bnj1230  31472  bnj1476  31516  bnj1204  31679  bnj1311  31691  sltval2  32398  bj-rabtrALT  33501  topdifinfindis  33789  icorempt2  33794  isbasisrelowllem1  33798  isbasisrelowllem2  33799  relowlssretop  33806  phpreu  34018  poimirlem26  34061  poimirlem27  34062  mbfposadd  34082  cover2  34133  rababg  38836  rfcnpre1  40111  rfcnpre2  40123  ssrab2f  40229  infnsuprnmpt  40376  allbutfiinf  40553  supminfxr2  40604  fsumiunss  40715  limcperiod  40768  fnlimcnv  40807  fnlimfvre2  40817  fnlimf  40818  limsupequzmpt2  40858  liminfequzmpt2  40931  dvcosre  41054  stoweidlem14  41158  stoweidlem26  41170  stoweidlem31  41175  stoweidlem34  41178  stoweidlem35  41179  stoweidlem46  41190  stoweidlem50  41194  stoweidlem51  41195  stoweidlem52  41196  stoweidlem53  41197  stoweidlem54  41198  stoweidlem57  41201  stoweidlem59  41203  fourierdlem20  41271  fourierdlem31  41282  fourierdlem79  41329  sge0iunmptlemre  41556  ovnlerp  41703  opnvonmbllem1  41773  preimagelt  41839  preimalegt  41840  pimconstlt1  41842  pimltpnf  41843  pimrecltpos  41846  pimiooltgt  41848  pimdecfgtioc  41852  pimincfltioc  41853  pimdecfgtioo  41854  pimincfltioo  41855  preimageiingt  41857  preimaleiinlt  41858  pimrecltneg  41860  sssmf  41874  incsmflem  41877  issmfle  41881  issmfgt  41892  smfaddlem1  41898  decsmflem  41901  issmfge  41905  smflimlem2  41907  smflim  41912  smfresal  41922  smfmullem2  41926  smfmullem4  41928  smfpimbor1lem2  41933  smflim2  41939  smfpimcclem  41940  smfsup  41947  smfinf  41951  smflimsuplem2  41954  smflimsuplem5  41957  smflimsuplem7  41959  smflimsup  41961  smfliminf  41964  prmdvdsfmtnof1lem1  42517