Theorem nfrab1 3384

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

Syntax hints:   ∧ wa 398   ∈ wcel 2114  {cab 2799  Ⅎwnfc 2961  {crab 3142

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147

This theorem is referenced by:  reusv2lem4  5302  reusv2  5304  rabxfrd  5318  riotaxfrd  7148  onminsb  7514  tfis  7569  oawordeulem  8180  nnawordex  8263  rankidb  9229  tskwe  9379  cardmin2  9427  cardaleph  9515  cardmin  9986  nnwos  12316  neiptopnei  21740  dissnlocfin  22137  imasnopn  22298  imasncld  22299  imasncls  22300  blval2  23172  iundisj  24149  mbfinf  24266  lfgrnloop  26910  difrab2  30261  rabexgfGS  30262  rabss3d  30276  iundisjf  30339  fimarab  30390  aciunf1  30408  fpwrelmap  30469  fpwrelmapffs  30470  iundisjfi  30519  locfinreflem  31104  ordtconnlem1  31167  esumrnmpt2  31327  esumpinfval  31332  hasheuni  31344  ldsysgenld  31419  measvuni  31473  eulerpartlemn  31639  ballotlem7  31793  ballotth  31795  reprdifc  31898  bnj1230  32074  bnj1476  32119  bnj1204  32284  bnj1311  32296  satfv1  32610  sltval2  33163  bj-rabtrALT  34252  topdifinfindis  34630  icorempo  34635  isbasisrelowllem1  34639  isbasisrelowllem2  34640  relowlssretop  34647  phpreu  34891  poimirlem26  34933  poimirlem27  34934  mbfposadd  34954  cover2  35004  rababg  39953  rfcnpre1  41296  rfcnpre2  41308  ssrab2f  41403  infnsuprnmpt  41542  allbutfiinf  41714  supminfxr2  41765  fsumiunss  41876  limcperiod  41929  fnlimcnv  41968  fnlimfvre2  41978  fnlimf  41979  limsupequzmpt2  42019  liminfequzmpt2  42092  dvcosre  42216  stoweidlem14  42319  stoweidlem26  42331  stoweidlem31  42336  stoweidlem34  42339  stoweidlem35  42340  stoweidlem46  42351  stoweidlem50  42355  stoweidlem51  42356  stoweidlem52  42357  stoweidlem53  42358  stoweidlem54  42359  stoweidlem57  42362  stoweidlem59  42364  fourierdlem20  42432  fourierdlem31  42443  fourierdlem79  42490  sge0iunmptlemre  42717  ovnlerp  42864  opnvonmbllem1  42934  preimagelt  43000  preimalegt  43001  pimconstlt1  43003  pimltpnf  43004  pimrecltpos  43007  pimiooltgt  43009  pimdecfgtioc  43013  pimincfltioc  43014  pimdecfgtioo  43015  pimincfltioo  43016  preimageiingt  43018  preimaleiinlt  43019  pimrecltneg  43021  sssmf  43035  incsmflem  43038  issmfle  43042  issmfgt  43053  smfaddlem1  43059  decsmflem  43062  issmfge  43066  smflimlem2  43068  smflim  43073  smfresal  43083  smfmullem2  43087  smfmullem4  43089  smfpimbor1lem2  43094  smflim2  43100  smfpimcclem  43101  smfsup  43108  smfinf  43112  smflimsuplem2  43115  smflimsuplem5  43118  smflimsuplem7  43120  smflimsup  43122  smfliminf  43125  prmdvdsfmtnof1lem1  43766