Theorem nffv 6680

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 6363	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2977	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5113	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6318	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2975	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2961   class class class wbr 5066  ℩cio 6312  ‘cfv 6355

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-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363

This theorem is referenced by:  nffvmpt1  6681  nffvd  6682  fvelimad  6732  dffn5f  6736  fvmptss  6780  fvmptex  6782  fvmptf  6789  fvmptnf  6790  eqfnfv2f  6806  ralrnmptw  6860  ralrnmpt  6862  ffnfvf  6883  funiunfvf  7008  dff13f  7014  nfiso  7075  nfwrecs  7949  nfrdg  8050  rdgsucmptf  8064  rdgsucmptnf  8065  frsucmpt  8073  frsucmptn  8074  rankidb  9229  rankval4  9296  dfac8clem  9458  cardaleph  9515  hsmexlem2  9849  axcc2  9859  uniimadomf  9967  nfseq  13380  seqof2  13429  rlim2  14853  nfsum1  15046  nfsumw  15047  nfsum  15048  sumeq2ii  15050  fsumrelem  15162  o1fsum  15168  nfcprod1  15264  nfcprod  15265  fprodefsum  15448  prdsbas3  16754  prdsdsval2  16757  yonedalem4b  17526  gsum2d2lem  19093  coe1fzgsumdlem  20469  evl1gsumdlem  20519  ptcldmpt  22222  ptcnp  22230  cnmpt11  22271  cnmpt21  22279  cnmptk2  22294  prdsdsf  22977  prdsxmet  22979  ovolfiniun  24102  ovoliunlem3  24105  ovoliun  24106  ovoliun2  24107  ovoliunnul  24108  volfiniun  24148  voliun  24155  mbfsup  24265  mbflim  24269  itg2splitlem  24349  itg2split  24350  itg2cnlem1  24362  isibl2  24367  nfitg1  24374  nfitg  24375  cbvitg  24376  itgabs  24435  dvlipcn  24591  lhop2  24612  dvfsumabs  24620  dvfsumrlim  24628  itgparts  24644  itgsubstlem  24645  ulmss  24985  itgulm2  24997  lgamgulmlem2  25607  lgamgulmlem6  25611  lgamgulm2  25613  lgseisenlem2  25952  dchrisumlem3  26067  cnlnadjlem5  29848  dfimafnf  30381  esumfzf  31328  voliune  31488  volfiniune  31489  bnj1534  32125  bnj1542  32129  bnj958  32212  bnj1000  32213  bnj1446  32317  bnj1447  32318  bnj1448  32319  bnj1466  32325  bnj1467  32326  bnj1519  32337  bnj1520  32338  bnj1529  32342  cvmcov  32510  trpredlem1  33066  trpredrec  33077  sltval2  33163  rdgssun  34662  exrecfnlem  34663  finxpreclem2  34674  finxpreclem6  34680  poimirlem23  34930  poimirlem27  34934  itgabsnc  34976  riotaocN  36360  cdleme32d  37595  cdleme32f  37597  ltrniotaval  37732  cdlemksv2  37998  cdlemkuv2  38018  cdlemk36  38064  cdlemk38  38066  cdlemk19x  38094  cdlemk11t  38097  mzpsubst  39394  aomclem8  39710  binomcxplemdvbinom  40734  binomcxplemdvsum  40736  binomcxplemnotnn0  40737  evth2f  41321  fvelrnbf  41324  evthf  41333  rfcnpre3  41339  rfcnpre4  41340  rfcnnnub  41342  refsum2cnlem1  41343  dffo3f  41487  allbutfiinf  41743  monoordxr  41808  monoord2xr  41810  fmul01  41910  fmuldfeqlem1  41912  fmuldfeq  41913  fmul01lt1lem1  41914  fmul01lt1lem2  41915  fmul01lt1  41916  cncfmptss  41917  mulc1cncfg  41919  expcnfg  41921  fprodabs2  41925  climmulf  41934  climexp  41935  climsuse  41938  climrecf  41939  climinff  41941  climaddf  41945  mullimc  41946  idlimc  41956  limcperiod  41958  neglimc  41977  addlimc  41978  0ellimcdiv  41979  fnlimfv  41993  climreclf  41994  fnlimcnv  41997  fnlimfvre  42004  fnlimfvre2  42007  fnlimf  42008  fnlimabslt  42009  climfveqf  42010  climmptf  42011  climeldmeqf  42013  limsupref  42015  limsupbnd1f  42016  climbddf  42017  climeqf  42018  limsuppnfd  42032  climinf2  42037  limsuppnf  42041  limsupubuz  42043  climinfmpt  42045  limsupmnf  42051  limsupequz  42053  limsupre2  42055  limsupmnfuz  42057  limsupre3  42063  limsupre3uz  42066  limsupreuz  42067  climuz  42074  lmbr3  42077  limsupgt  42108  liminfvalxr  42113  liminfreuz  42133  liminflt  42135  xlimpnfxnegmnf  42144  liminfpnfuz  42146  xlimmnf  42171  xlimpnf  42172  dfxlim2  42178  xlimpnfxnegmnf2  42188  cncfshift  42206  icccncfext  42219  cncficcgt0  42220  cncfiooicclem1  42225  dvnmul  42277  dvnprodlem1  42280  itgsubsticclem  42309  stoweidlem3  42337  stoweidlem23  42357  stoweidlem26  42360  stoweidlem28  42362  stoweidlem29  42363  stoweidlem31  42365  stoweidlem34  42368  stoweidlem36  42370  stoweidlem42  42376  stoweidlem48  42382  stoweidlem51  42385  stoweidlem52  42386  stoweidlem59  42393  wallispilem5  42403  stirlinglem4  42411  stirlinglem11  42418  stirlinglem12  42419  stirlinglem13  42420  stirlinglem14  42421  stirlinglem15  42422  fourierdlem20  42461  fourierdlem31  42472  fourierdlem79  42519  fourierdlem89  42529  fourierdlem91  42531  fourierdlem112  42552  fourierdlem115  42555  fourierd  42556  fourierclimd  42557  etransclem2  42570  etransclem48  42616  sge0revalmpt  42709  sge0fsummpt  42721  sge0iunmptlemfi  42744  sge0iunmptlemre  42746  sge0iunmpt  42749  sge0xadd  42766  sge0fsummptf  42767  sge0gtfsumgt  42774  iundjiun  42791  meadjiun  42797  voliunsge0lem  42803  meaiunincf  42814  meaiuninc3  42816  omeiunle  42848  omeiunltfirp  42850  ovncvrrp  42895  vonioo  43013  vonicc  43016  vonn0ioo2  43021  vonn0icc2  43023  pimltmnf2  43028  pimgtpnf2  43034  pimltpnf2  43040  pimgtmnf2  43041  pimdecfgtioc  43042  issmff  43060  smfpimltxrmpt  43084  smfpreimagtf  43093  smflim  43102  smfpimgtxr  43105  smfpimgtxrmpt  43109  smfmullem4  43118  smflim2  43129  smfpimcclem  43130  smfpimcc  43131  smfsup  43137  smfsupmpt  43138  smfsupxr  43139  smfinflem  43140  smfinf  43141  smfinfmpt  43142  smflimsuplem2  43144  smflimsuplem5  43147  smflimsuplem7  43149  smflimsup  43151  smfliminf  43154  nfafv  43384  nfsetrecs  44838  setrec2fun  44844