Theorem nfrab1 3435

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2147  {cab 2741  Ⅎwnfc 2911  {crab 3416

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-rab 3417

This theorem is used by:  rabss3d  4009  eqrrabd  4014  reusv2lem4  5370  reusv2  5372  rabxfrd  5386  fimarab  6990  riotaxfrd  7442  onminsb  7842  tfis  7900  oawordeulem  8600  nnawordex  8684  rankidb  9845  tskwe  10068  cardmin2  10119  cardaleph  10207  cardmin  10687  nnwos  13082  rspsn0  21577  neiptopnei  23505  dissnlocfin  23903  imasnopn  24064  imasncld  24065  imasncls  24066  blval2  24936  iundisj  25924  mbfinf  26041  ltsval2  28070  lfgrnloop  29760  difrab2  33193  rabexgfGS  33194  iundisjf  33281  aciunf1  33355  fpwrelmap  33421  fpwrelmapffs  33422  iundisjfi  33484  algextdeglem6  34465  constrfin  34489  locfinreflem  34583  zarcls  34617  ordtconnlem1  34667  esumrnmpt2  34811  esumpinfval  34816  hasheuni  34828  ldsysgenld  34904  measvuni  34958  eulerpartlemn  35124  ballotlem7  35279  ballotth  35281  reprdifc  35367  bnj1230  35543  bnj1476  35588  bnj1204  35753  bnj1311  35765  onvf1odlem2  36073  onprcf1acwevdlem2  36087  vonf1oonfo  36090  onprcf1of1ord  36096  satfv1  36336  bj-rabtrALT  38059  topdifinfindis  38537  icorempo  38542  isbasisrelowllem1  38546  isbasisrelowllem2  38547  relowlssretop  38554  phpreu  38795  poimirlem26  38832  poimirlem27  38833  mbfposadd  38853  cover2  38917  naddwordnexlem4  44664  rababg  44836  permaxsep  46261  rfcnpre1  46310  rfcnpre2  46322  ssrab2f  46405  infnsuprnmpt  46535  allbutfiinf  46703  supminfxr2  46752  pimxrneun  46771  limcperiod  46913  fnlimcnv  46950  fnlimfvre2  46960  fnlimf  46961  limsupequzmpt2  47001  liminfequzmpt2  47074  dvcosre  47195  stoweidlem14  47297  stoweidlem26  47309  stoweidlem31  47314  stoweidlem34  47317  stoweidlem35  47318  stoweidlem46  47329  stoweidlem50  47333  stoweidlem51  47334  stoweidlem52  47335  stoweidlem53  47336  stoweidlem54  47337  stoweidlem57  47340  stoweidlem59  47342  fourierdlem20  47410  fourierdlem31  47421  fourierdlem79  47468  sge0iunmptlemre  47698  ovnlerp  47845  opnvonmbllem1  47915  preimagelt  47982  preimalegt  47983  pimconstlt1  47985  pimltpnff  47986  pimrecltpos  47991  pimiooltgt  47993  pimdecfgtioc  47998  pimincfltioc  47999  pimdecfgtioo  48000  pimincfltioo  48001  preimageiingt  48003  preimaleiinlt  48004  pimgtmnff  48005  pimrecltneg  48007  sssmf  48021  incsmflem  48024  issmfle  48028  issmfgt  48039  smfaddlem1  48046  decsmflem  48049  issmfge  48053  smflimlem2  48055  smflim  48060  smfresal  48071  smfmullem2  48075  smfmullem4  48077  smfpimbor1lem2  48082  smflim2  48089  smfpimcclem  48090  smfsup  48097  smfinf  48101  smflimsuplem2  48104  smflimsuplem5  48107  smflimsuplem7  48109  smflimsup  48111  smfliminf  48114  smfdivdmmbl2  48124  fsupdm  48125  fsupdm2  48126  finfdm  48129  finfdm2  48130  prmdvdsfmtnof1lem1  48942