Theorem nffv 6891

Description: Bound-variable hypothesis builder for function value. (Contributed by NM, 14-Nov-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)

Hypotheses

Ref	Expression
nffv.1	⊢ Ⅎ𝑥𝐹
nffv.2	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
nffv	⊢ Ⅎ𝑥(𝐹‘𝐴)

Proof of Theorem nffv

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-fv 6544	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2925	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5158	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6496	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2923	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2910   class class class wbr 5109  ℩cio 6490  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544

This theorem is referenced by:  nffvmpt1  6892  nffvd  6893  fvelimad  6948  dffn5f  6952  fvmptss  7002  fvmptex  7004  fvmptf  7011  fvmptnf  7012  eqfnfv2f  7029  ralrnmptw  7089  ralrnmpt  7091  dffo3f  7101  ffnfvf  7115  funiunfvf  7247  dff13f  7253  nfiso  7320  nfrdg  8397  rdgsucmptf  8411  rdgsucmptnf  8412  frsucmpt  8421  frsucmptn  8422  ttrclselem1  9690  ttrclselem2  9691  rankidb  9768  rankval4  9835  dfac8clem  10012  cardaleph  10069  hsmexlem2  10406  axcc2  10416  uniimadomf  10524  nfseq  14043  seqof2  14092  rlim2  15543  nfsum1  15737  nfsum  15738  sumeq2ii  15740  fsumrelem  15855  o1fsum  15861  nfcprod1  15958  nfcprod  15959  fprodefsum  16144  prdsbas3  17529  prdsdsval2  17532  yonedalem4b  18327  gsum2d2lem  20038  coe1fzgsumdlem  22463  evl1gsumdlem  22516  ptcldmpt  23771  ptcnp  23779  cnmpt11  23820  cnmpt21  23828  cnmptk2  23843  prdsdsf  24524  prdsxmet  24526  ovolfiniun  25660  ovoliunlem3  25663  ovoliun  25664  ovoliun2  25665  ovoliunnul  25666  volfiniun  25706  voliun  25713  mbfsup  25823  mbflim  25827  itg2splitlem  25907  itg2split  25908  itg2cnlem1  25920  isibl2  25925  nfitg1  25933  nfitg  25934  cbvitg  25935  itgabs  25994  dvlipcn  26153  lhop2  26174  dvfsumabs  26182  dvfsumrlim  26190  itgparts  26206  itgsubstlem  26207  ulmss  26560  itgulm2  26572  lgamgulmlem2  27194  lgamgulmlem6  27198  lgamgulm2  27200  lgseisenlem2  27540  dchrisumlem3  27655  ltsval2  27820  nfseqs  28480  cnlnadjlem5  32423  dfimafnf  32981  2ndresdju  32994  deg1prod  33873  esumfzf  34459  voliune  34619  volfiniune  34620  bnj1534  35241  bnj1542  35245  bnj958  35328  bnj1000  35329  bnj1446  35433  bnj1447  35434  bnj1448  35435  bnj1466  35441  bnj1467  35442  bnj1519  35453  bnj1520  35454  bnj1529  35458  rankval4b  35493  onvf1odlem2  35588  vonf1oonfo  35599  cvmcov  35755  rdgssun  38024  exrecfnlem  38025  finxpreclem2  38036  finxpreclem6  38042  poimirlem23  38294  poimirlem27  38298  itgabsnc  38340  riotaocN  39983  cdleme32d  41218  cdleme32f  41220  ltrniotaval  41355  cdlemksv2  41621  cdlemkuv2  41641  cdlemk36  41687  cdlemk38  41689  cdlemk19x  41717  cdlemk11t  41720  evl1gprodd  42884  mzpsubst  43479  aomclem8  43788  mnringmulrcld  44952  binomcxplemdvbinom  45063  binomcxplemdvsum  45065  binomcxplemnotnn0  45066  nfrelp  45658  permaxrep  45715  permaxsep  45716  evth2f  45735  fvelrnbf  45738  evthf  45747  rfcnpre3  45753  rfcnpre4  45754  rfcnnnub  45756  refsum2cnlem1  45757  allbutfiinf  46134  monoordxr  46196  monoord2xr  46198  caucvgbf  46203  cvgcaule  46205  fmul01  46296  fmuldfeqlem1  46298  fmuldfeq  46299  fmul01lt1lem1  46300  fmul01lt1lem2  46301  fmul01lt1  46302  cncfmptss  46303  mulc1cncfg  46305  expcnfg  46307  fprodabs2  46311  climmulf  46320  climexp  46321  climsuse  46324  climrecf  46325  climinff  46327  climaddf  46331  mullimc  46332  idlimc  46342  limcperiod  46344  neglimc  46361  addlimc  46362  0ellimcdiv  46363  fnlimfv  46377  climreclf  46378  fnlimcnv  46381  fnlimfvre  46388  fnlimfvre2  46391  fnlimf  46392  fnlimabslt  46393  climfveqf  46394  climmptf  46395  climeldmeqf  46397  limsupref  46399  limsupbnd1f  46400  climbddf  46401  climeqf  46402  limsuppnfd  46416  climinf2  46421  limsuppnf  46425  limsupubuz  46427  climinfmpt  46429  limsupmnf  46435  limsupequz  46437  limsupre2  46439  limsupmnfuz  46441  limsupre3  46447  limsupre3uz  46450  limsupreuz  46451  climuz  46458  lmbr3  46461  limsupgt  46492  liminfvalxr  46497  liminfreuz  46517  liminflt  46519  xlimpnfxnegmnf  46528  liminfpnfuz  46530  xlimmnf  46555  xlimpnf  46556  dfxlim2  46562  xlimpnfxnegmnf2  46572  cncfshift  46588  icccncfext  46601  cncficcgt0  46602  cncfiooicclem1  46607  dvnmul  46657  dvnprodlem1  46660  itgsubsticclem  46689  stoweidlem3  46717  stoweidlem23  46737  stoweidlem26  46740  stoweidlem28  46742  stoweidlem29  46743  stoweidlem31  46745  stoweidlem34  46748  stoweidlem36  46750  stoweidlem42  46756  stoweidlem48  46762  stoweidlem51  46765  stoweidlem52  46766  stoweidlem59  46773  wallispilem5  46783  stirlinglem4  46791  stirlinglem11  46798  stirlinglem12  46799  stirlinglem13  46800  stirlinglem14  46801  stirlinglem15  46802  fourierdlem20  46841  fourierdlem31  46852  fourierdlem79  46899  fourierdlem89  46909  fourierdlem91  46911  fourierdlem112  46932  fourierdlem115  46935  fourierd  46936  fourierclimd  46937  etransclem2  46950  etransclem48  46996  sge0revalmpt  47092  sge0fsummpt  47104  sge0iunmptlemfi  47127  sge0iunmptlemre  47129  sge0iunmpt  47132  sge0xadd  47149  sge0fsummptf  47150  sge0gtfsumgt  47157  iundjiun  47174  meadjiun  47180  voliunsge0lem  47186  meaiunincf  47197  meaiuninc3  47199  omeiunle  47231  omeiunltfirp  47233  ovncvrrp  47278  vonioo  47396  vonicc  47399  vonn0ioo2  47404  vonn0icc2  47406  pimltmnf2f  47411  pimgtpnf2f  47419  pimltpnf2f  47426  pimgtmnf2  47428  pimdecfgtioc  47429  issmff  47448  smfpimltxrmptf  47472  smfpreimagtf  47482  smflim  47491  smfpimgtxr  47494  smfpimgtxrmptf  47498  smfmullem4  47508  smflim2  47520  smfpimcclem  47521  smfpimcc  47522  smfsup  47528  smfsupmpt  47529  smfsupxr  47530  smfinflem  47531  smfinf  47532  smflimsuplem2  47535  smflimsuplem5  47538  smflimsuplem7  47540  smflimsup  47542  smfliminf  47545  fsupdm  47556  smfsupdmmbllem  47558  finfdm  47560  smfinfdmmbllem  47562  nfafv  47873  nfsetrecs  50464  setrec2fun  50470