Theorem nfrab1 3410

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

Syntax hints:   ∧ wa 395   ∈ wcel 2114  {cab 2715  Ⅎwnfc 2884  {crab 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rab 3391

This theorem is referenced by:  rabss3d  4022  eqrrabd  4027  reusv2lem4  5338  reusv2  5340  rabxfrd  5354  fimarab  6908  riotaxfrd  7351  onminsb  7741  tfis  7799  oawordeulem  8482  nnawordex  8566  rankidb  9715  tskwe  9865  cardmin2  9914  cardaleph  10002  cardmin  10477  nnwos  12856  neiptopnei  23107  dissnlocfin  23504  imasnopn  23665  imasncld  23666  imasncls  23667  blval2  24537  iundisj  25525  mbfinf  25642  ltsval2  27634  lfgrnloop  29208  difrab2  32582  rabexgfGS  32584  iundisjf  32674  aciunf1  32751  fpwrelmap  32821  fpwrelmapffs  32822  iundisjfi  32884  algextdeglem6  33882  constrfin  33906  locfinreflem  34000  zarcls  34034  ordtconnlem1  34084  esumrnmpt2  34228  esumpinfval  34233  hasheuni  34245  ldsysgenld  34320  measvuni  34374  eulerpartlemn  34541  ballotlem7  34696  ballotth  34698  reprdifc  34787  bnj1230  34960  bnj1476  35005  bnj1204  35170  bnj1311  35182  onvf1odlem2  35302  satfv1  35561  bj-rabtrALT  37254  topdifinfindis  37676  icorempo  37681  isbasisrelowllem1  37685  isbasisrelowllem2  37686  relowlssretop  37693  phpreu  37939  poimirlem26  37981  poimirlem27  37982  mbfposadd  38002  cover2  38050  naddwordnexlem4  43847  rababg  44019  permaxsep  45452  rfcnpre1  45468  rfcnpre2  45480  ssrab2f  45565  infnsuprnmpt  45697  allbutfiinf  45866  supminfxr2  45915  pimxrneun  45934  limcperiod  46076  fnlimcnv  46113  fnlimfvre2  46123  fnlimf  46124  limsupequzmpt2  46164  liminfequzmpt2  46237  dvcosre  46358  stoweidlem14  46460  stoweidlem26  46472  stoweidlem31  46477  stoweidlem34  46480  stoweidlem35  46481  stoweidlem46  46492  stoweidlem50  46496  stoweidlem51  46497  stoweidlem52  46498  stoweidlem53  46499  stoweidlem54  46500  stoweidlem57  46503  stoweidlem59  46505  fourierdlem20  46573  fourierdlem31  46584  fourierdlem79  46631  sge0iunmptlemre  46861  ovnlerp  47008  opnvonmbllem1  47078  preimagelt  47145  preimalegt  47146  pimconstlt1  47148  pimltpnff  47149  pimrecltpos  47154  pimiooltgt  47156  pimdecfgtioc  47161  pimincfltioc  47162  pimdecfgtioo  47163  pimincfltioo  47164  preimageiingt  47166  preimaleiinlt  47167  pimgtmnff  47168  pimrecltneg  47170  sssmf  47184  incsmflem  47187  issmfle  47191  issmfgt  47202  smfaddlem1  47209  decsmflem  47212  issmfge  47216  smflimlem2  47218  smflim  47223  smfresal  47234  smfmullem2  47238  smfmullem4  47240  smfpimbor1lem2  47245  smflim2  47252  smfpimcclem  47253  smfsup  47260  smfinf  47264  smflimsuplem2  47267  smflimsuplem5  47270  smflimsuplem7  47272  smflimsup  47274  smfliminf  47277  smfdivdmmbl2  47287  fsupdm  47288  fsupdm2  47289  finfdm  47292  finfdm2  47293  prmdvdsfmtnof1lem1  48059