Theorem nffv 6766

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 6426	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2906	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5117	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6380	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2904	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2886   class class class wbr 5070  ℩cio 6374  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426

This theorem is referenced by:  nffvmpt1  6767  nffvd  6768  fvelimad  6818  dffn5f  6822  fvmptss  6869  fvmptex  6871  fvmptf  6878  fvmptnf  6879  eqfnfv2f  6895  ralrnmptw  6952  ralrnmpt  6954  ffnfvf  6975  funiunfvf  7104  dff13f  7110  nfiso  7173  nfwrecsOLD  8104  nfrdg  8216  rdgsucmptf  8230  rdgsucmptnf  8231  frsucmpt  8239  frsucmptn  8240  trpredlem1  9405  trpredrec  9415  rankidb  9489  rankval4  9556  dfac8clem  9719  cardaleph  9776  hsmexlem2  10114  axcc2  10124  uniimadomf  10232  nfseq  13659  seqof2  13709  rlim2  15133  nfsum1  15329  nfsum  15330  nfsumOLD  15331  sumeq2ii  15333  fsumrelem  15447  o1fsum  15453  nfcprod1  15548  nfcprod  15549  fprodefsum  15732  prdsbas3  17109  prdsdsval2  17112  yonedalem4b  17910  gsum2d2lem  19489  coe1fzgsumdlem  21382  evl1gsumdlem  21432  ptcldmpt  22673  ptcnp  22681  cnmpt11  22722  cnmpt21  22730  cnmptk2  22745  prdsdsf  23428  prdsxmet  23430  ovolfiniun  24570  ovoliunlem3  24573  ovoliun  24574  ovoliun2  24575  ovoliunnul  24576  volfiniun  24616  voliun  24623  mbfsup  24733  mbflim  24737  itg2splitlem  24818  itg2split  24819  itg2cnlem1  24831  isibl2  24836  nfitg1  24843  nfitg  24844  cbvitg  24845  itgabs  24904  dvlipcn  25063  lhop2  25084  dvfsumabs  25092  dvfsumrlim  25100  itgparts  25116  itgsubstlem  25117  ulmss  25461  itgulm2  25473  lgamgulmlem2  26084  lgamgulmlem6  26088  lgamgulm2  26090  lgseisenlem2  26429  dchrisumlem3  26544  cnlnadjlem5  30334  dfimafnf  30872  2ndresdju  30887  esumfzf  31937  voliune  32097  volfiniune  32098  bnj1534  32733  bnj1542  32737  bnj958  32820  bnj1000  32821  bnj1446  32925  bnj1447  32926  bnj1448  32927  bnj1466  32933  bnj1467  32934  bnj1519  32945  bnj1520  32946  bnj1529  32950  cvmcov  33125  ttrclselem1  33711  ttrclselem2  33712  sltval2  33786  rdgssun  35476  exrecfnlem  35477  finxpreclem2  35488  finxpreclem6  35494  poimirlem23  35727  poimirlem27  35731  itgabsnc  35773  riotaocN  37150  cdleme32d  38385  cdleme32f  38387  ltrniotaval  38522  cdlemksv2  38788  cdlemkuv2  38808  cdlemk36  38854  cdlemk38  38856  cdlemk19x  38884  cdlemk11t  38887  mzpsubst  40486  aomclem8  40802  mnringmulrcld  41735  binomcxplemdvbinom  41860  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  evth2f  42447  fvelrnbf  42450  evthf  42459  rfcnpre3  42465  rfcnpre4  42466  rfcnnnub  42468  refsum2cnlem1  42469  dffo3f  42606  allbutfiinf  42850  monoordxr  42913  monoord2xr  42915  fmul01  43011  fmuldfeqlem1  43013  fmuldfeq  43014  fmul01lt1lem1  43015  fmul01lt1lem2  43016  fmul01lt1  43017  cncfmptss  43018  mulc1cncfg  43020  expcnfg  43022  fprodabs2  43026  climmulf  43035  climexp  43036  climsuse  43039  climrecf  43040  climinff  43042  climaddf  43046  mullimc  43047  idlimc  43057  limcperiod  43059  neglimc  43078  addlimc  43079  0ellimcdiv  43080  fnlimfv  43094  climreclf  43095  fnlimcnv  43098  fnlimfvre  43105  fnlimfvre2  43108  fnlimf  43109  fnlimabslt  43110  climfveqf  43111  climmptf  43112  climeldmeqf  43114  limsupref  43116  limsupbnd1f  43117  climbddf  43118  climeqf  43119  limsuppnfd  43133  climinf2  43138  limsuppnf  43142  limsupubuz  43144  climinfmpt  43146  limsupmnf  43152  limsupequz  43154  limsupre2  43156  limsupmnfuz  43158  limsupre3  43164  limsupre3uz  43167  limsupreuz  43168  climuz  43175  lmbr3  43178  limsupgt  43209  liminfvalxr  43214  liminfreuz  43234  liminflt  43236  xlimpnfxnegmnf  43245  liminfpnfuz  43247  xlimmnf  43272  xlimpnf  43273  dfxlim2  43279  xlimpnfxnegmnf2  43289  cncfshift  43305  icccncfext  43318  cncficcgt0  43319  cncfiooicclem1  43324  dvnmul  43374  dvnprodlem1  43377  itgsubsticclem  43406  stoweidlem3  43434  stoweidlem23  43454  stoweidlem26  43457  stoweidlem28  43459  stoweidlem29  43460  stoweidlem31  43462  stoweidlem34  43465  stoweidlem36  43467  stoweidlem42  43473  stoweidlem48  43479  stoweidlem51  43482  stoweidlem52  43483  stoweidlem59  43490  wallispilem5  43500  stirlinglem4  43508  stirlinglem11  43515  stirlinglem12  43516  stirlinglem13  43517  stirlinglem14  43518  stirlinglem15  43519  fourierdlem20  43558  fourierdlem31  43569  fourierdlem79  43616  fourierdlem89  43626  fourierdlem91  43628  fourierdlem112  43649  fourierdlem115  43652  fourierd  43653  fourierclimd  43654  etransclem2  43667  etransclem48  43713  sge0revalmpt  43806  sge0fsummpt  43818  sge0iunmptlemfi  43841  sge0iunmptlemre  43843  sge0iunmpt  43846  sge0xadd  43863  sge0fsummptf  43864  sge0gtfsumgt  43871  iundjiun  43888  meadjiun  43894  voliunsge0lem  43900  meaiunincf  43911  meaiuninc3  43913  omeiunle  43945  omeiunltfirp  43947  ovncvrrp  43992  vonioo  44110  vonicc  44113  vonn0ioo2  44118  vonn0icc2  44120  pimltmnf2  44125  pimgtpnf2  44131  pimltpnf2  44137  pimgtmnf2  44138  pimdecfgtioc  44139  issmff  44157  smfpimltxrmpt  44181  smfpreimagtf  44190  smflim  44199  smfpimgtxr  44202  smfpimgtxrmpt  44206  smfmullem4  44215  smflim2  44226  smfpimcclem  44227  smfpimcc  44228  smfsup  44234  smfsupmpt  44235  smfsupxr  44236  smfinflem  44237  smfinf  44238  smfinfmpt  44239  smflimsuplem2  44241  smflimsuplem5  44244  smflimsuplem7  44246  smflimsup  44248  smfliminf  44251  nfafv  44515  nfsetrecs  46278  setrec2fun  46284