Theorem nfrab1 3432

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2145  {cab 2739  Ⅎwnfc 2908  {crab 3413

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-rab 3414

This theorem is used by:  rabss3d  4029  eqrrabd  4034  reusv2lem4  5363  reusv2  5365  rabxfrd  5379  fimarab  6957  riotaxfrd  7409  onminsb  7806  tfis  7864  oawordeulem  8555  nnawordex  8639  rankidb  9801  tskwe  10024  cardmin2  10073  cardaleph  10161  cardmin  10641  nnwos  13035  rspsn0  21519  neiptopnei  23443  dissnlocfin  23841  imasnopn  24002  imasncld  24003  imasncls  24004  blval2  24874  iundisj  25862  mbfinf  25979  ltsval2  28006  lfgrnloop  29696  difrab2  33087  rabexgfGS  33088  iundisjf  33176  aciunf1  33250  fpwrelmap  33318  fpwrelmapffs  33319  iundisjfi  33381  algextdeglem6  34347  constrfin  34371  locfinreflem  34465  zarcls  34499  ordtconnlem1  34549  esumrnmpt2  34693  esumpinfval  34698  hasheuni  34710  ldsysgenld  34786  measvuni  34840  eulerpartlemn  35006  ballotlem7  35161  ballotth  35163  reprdifc  35249  bnj1230  35425  bnj1476  35470  bnj1204  35635  bnj1311  35647  onvf1odlem2  35866  vonf1oonfo  35877  satfv1  36107  bj-rabtrALT  37824  topdifinfindis  38249  icorempo  38254  isbasisrelowllem1  38258  isbasisrelowllem2  38259  relowlssretop  38266  phpreu  38507  poimirlem26  38544  poimirlem27  38545  mbfposadd  38565  cover2  38629  naddwordnexlem4  44387  rababg  44559  permaxsep  45975  rfcnpre1  46005  rfcnpre2  46017  ssrab2f  46101  infnsuprnmpt  46231  allbutfiinf  46399  supminfxr2  46448  pimxrneun  46467  limcperiod  46609  fnlimcnv  46646  fnlimfvre2  46656  fnlimf  46657  limsupequzmpt2  46697  liminfequzmpt2  46770  dvcosre  46891  stoweidlem14  46993  stoweidlem26  47005  stoweidlem31  47010  stoweidlem34  47013  stoweidlem35  47014  stoweidlem46  47025  stoweidlem50  47029  stoweidlem51  47030  stoweidlem52  47031  stoweidlem53  47032  stoweidlem54  47033  stoweidlem57  47036  stoweidlem59  47038  fourierdlem20  47106  fourierdlem31  47117  fourierdlem79  47164  sge0iunmptlemre  47394  ovnlerp  47541  opnvonmbllem1  47611  preimagelt  47678  preimalegt  47679  pimconstlt1  47681  pimltpnff  47682  pimrecltpos  47687  pimiooltgt  47689  pimdecfgtioc  47694  pimincfltioc  47695  pimdecfgtioo  47696  pimincfltioo  47697  preimageiingt  47699  preimaleiinlt  47700  pimgtmnff  47701  pimrecltneg  47703  sssmf  47717  incsmflem  47720  issmfle  47724  issmfgt  47735  smfaddlem1  47742  decsmflem  47745  issmfge  47749  smflimlem2  47751  smflim  47756  smfresal  47767  smfmullem2  47771  smfmullem4  47773  smfpimbor1lem2  47778  smflim2  47785  smfpimcclem  47786  smfsup  47793  smfinf  47797  smflimsuplem2  47800  smflimsuplem5  47803  smflimsuplem7  47805  smflimsup  47807  smfliminf  47810  smfdivdmmbl2  47820  fsupdm  47821  fsupdm2  47822  finfdm  47825  finfdm2  47826  prmdvdsfmtnof1lem1  48638