Theorem nffv 6892

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 6545	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2931	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5162	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6497	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2929	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2916   class class class wbr 5113  ℩cio 6491  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545

This theorem is referenced by:  nffvmpt1  6893  nffvd  6894  fvelimad  6949  dffn5f  6953  fvmptss  7003  fvmptex  7005  fvmptf  7012  fvmptnf  7013  eqfnfv2f  7030  ralrnmptw  7090  ralrnmpt  7092  dffo3f  7102  ffnfvf  7116  funiunfvf  7248  dff13f  7254  nfiso  7321  nfrdg  8400  rdgsucmptf  8414  rdgsucmptnf  8415  frsucmpt  8424  frsucmptn  8425  ttrclselem1  9693  ttrclselem2  9694  rankidb  9771  rankval4  9838  dfac8clem  10015  cardaleph  10072  hsmexlem2  10410  axcc2  10420  uniimadomf  10528  nfseq  14046  seqof2  14095  rlim2  15546  nfsum1  15740  nfsum  15741  sumeq2ii  15743  fsumrelem  15858  o1fsum  15864  nfcprod1  15961  nfcprod  15962  fprodefsum  16148  prdsbas3  17533  prdsdsval2  17536  yonedalem4b  18331  gsum2d2lem  20042  coe1fzgsumdlem  22431  evl1gsumdlem  22484  ptcldmpt  23739  ptcnp  23747  cnmpt11  23788  cnmpt21  23796  cnmptk2  23811  prdsdsf  24492  prdsxmet  24494  ovolfiniun  25628  ovoliunlem3  25631  ovoliun  25632  ovoliun2  25633  ovoliunnul  25634  volfiniun  25674  voliun  25681  mbfsup  25791  mbflim  25795  itg2splitlem  25875  itg2split  25876  itg2cnlem1  25888  isibl2  25893  nfitg1  25901  nfitg  25902  cbvitg  25903  itgabs  25962  dvlipcn  26121  lhop2  26142  dvfsumabs  26150  dvfsumrlim  26158  itgparts  26174  itgsubstlem  26175  ulmss  26525  itgulm2  26537  lgamgulmlem2  27159  lgamgulmlem6  27163  lgamgulm2  27165  lgseisenlem2  27505  dchrisumlem3  27620  ltsval2  27785  nfseqs  28445  cnlnadjlem5  32363  dfimafnf  32921  2ndresdju  32934  deg1prod  33817  esumfzf  34403  voliune  34563  volfiniune  34564  bnj1534  35185  bnj1542  35189  bnj958  35272  bnj1000  35273  bnj1446  35377  bnj1447  35378  bnj1448  35379  bnj1466  35385  bnj1467  35386  bnj1519  35397  bnj1520  35398  bnj1529  35402  rankval4b  35435  onvf1odlem2  35486  vonf1oonfo  35497  cvmcov  35653  rdgssun  37911  exrecfnlem  37912  finxpreclem2  37923  finxpreclem6  37929  poimirlem23  38181  poimirlem27  38185  itgabsnc  38227  riotaocN  39872  cdleme32d  41107  cdleme32f  41109  ltrniotaval  41244  cdlemksv2  41510  cdlemkuv2  41530  cdlemk36  41576  cdlemk38  41578  cdlemk19x  41606  cdlemk11t  41609  evl1gprodd  42773  mzpsubst  43370  aomclem8  43679  mnringmulrcld  44843  binomcxplemdvbinom  44954  binomcxplemdvsum  44956  binomcxplemnotnn0  44957  nfrelp  45549  permaxrep  45606  permaxsep  45607  evth2f  45626  fvelrnbf  45629  evthf  45638  rfcnpre3  45644  rfcnpre4  45645  rfcnnnub  45647  refsum2cnlem1  45648  allbutfiinf  46025  monoordxr  46087  monoord2xr  46089  caucvgbf  46094  cvgcaule  46096  fmul01  46187  fmuldfeqlem1  46189  fmuldfeq  46190  fmul01lt1lem1  46191  fmul01lt1lem2  46192  fmul01lt1  46193  cncfmptss  46194  mulc1cncfg  46196  expcnfg  46198  fprodabs2  46202  climmulf  46211  climexp  46212  climsuse  46215  climrecf  46216  climinff  46218  climaddf  46222  mullimc  46223  idlimc  46233  limcperiod  46235  neglimc  46252  addlimc  46253  0ellimcdiv  46254  fnlimfv  46268  climreclf  46269  fnlimcnv  46272  fnlimfvre  46279  fnlimfvre2  46282  fnlimf  46283  fnlimabslt  46284  climfveqf  46285  climmptf  46286  climeldmeqf  46288  limsupref  46290  limsupbnd1f  46291  climbddf  46292  climeqf  46293  limsuppnfd  46307  climinf2  46312  limsuppnf  46316  limsupubuz  46318  climinfmpt  46320  limsupmnf  46326  limsupequz  46328  limsupre2  46330  limsupmnfuz  46332  limsupre3  46338  limsupre3uz  46341  limsupreuz  46342  climuz  46349  lmbr3  46352  limsupgt  46383  liminfvalxr  46388  liminfreuz  46408  liminflt  46410  xlimpnfxnegmnf  46419  liminfpnfuz  46421  xlimmnf  46446  xlimpnf  46447  dfxlim2  46453  xlimpnfxnegmnf2  46463  cncfshift  46479  icccncfext  46492  cncficcgt0  46493  cncfiooicclem1  46498  dvnmul  46548  dvnprodlem1  46551  itgsubsticclem  46580  stoweidlem3  46608  stoweidlem23  46628  stoweidlem26  46631  stoweidlem28  46633  stoweidlem29  46634  stoweidlem31  46636  stoweidlem34  46639  stoweidlem36  46641  stoweidlem42  46647  stoweidlem48  46653  stoweidlem51  46656  stoweidlem52  46657  stoweidlem59  46664  wallispilem5  46674  stirlinglem4  46682  stirlinglem11  46689  stirlinglem12  46690  stirlinglem13  46691  stirlinglem14  46692  stirlinglem15  46693  fourierdlem20  46732  fourierdlem31  46743  fourierdlem79  46790  fourierdlem89  46800  fourierdlem91  46802  fourierdlem112  46823  fourierdlem115  46826  fourierd  46827  fourierclimd  46828  etransclem2  46841  etransclem48  46887  sge0revalmpt  46983  sge0fsummpt  46995  sge0iunmptlemfi  47018  sge0iunmptlemre  47020  sge0iunmpt  47023  sge0xadd  47040  sge0fsummptf  47041  sge0gtfsumgt  47048  iundjiun  47065  meadjiun  47071  voliunsge0lem  47077  meaiunincf  47088  meaiuninc3  47090  omeiunle  47122  omeiunltfirp  47124  ovncvrrp  47169  vonioo  47287  vonicc  47290  vonn0ioo2  47295  vonn0icc2  47297  pimltmnf2f  47302  pimgtpnf2f  47310  pimltpnf2f  47317  pimgtmnf2  47319  pimdecfgtioc  47320  issmff  47339  smfpimltxrmptf  47363  smfpreimagtf  47373  smflim  47382  smfpimgtxr  47385  smfpimgtxrmptf  47389  smfmullem4  47399  smflim2  47411  smfpimcclem  47412  smfpimcc  47413  smfsup  47419  smfsupmpt  47420  smfsupxr  47421  smfinflem  47422  smfinf  47423  smflimsuplem2  47426  smflimsuplem5  47429  smflimsuplem7  47431  smflimsup  47433  smfliminf  47436  fsupdm  47447  smfsupdmmbllem  47449  finfdm  47451  smfinfdmmbllem  47453  nfafv  47761  nfsetrecs  50348  setrec2fun  50354