Theorem nffv 6110

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 5812	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2751	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 4629	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiota 5772	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2749	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2738   class class class wbr 4583  ℩cio 5766  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812

This theorem is referenced by:  nffvmpt1  6111  nffvd  6112  dffn5f  6162  fvmptss  6201  fvmptex  6203  fvmptf  6209  fvmptnf  6210  eqfnfv2f  6223  ralrnmpt  6276  ffnfvf  6296  funiunfvf  6411  dff13f  6417  nfiso  6472  nfwrecs  7296  nfrdg  7397  rdgsucmptf  7411  rdgsucmptnf  7412  frsucmpt  7420  frsucmptn  7421  rankidb  8546  rankval4  8613  dfac8clem  8738  cardaleph  8795  hsmexlem2  9132  axcc2  9142  uniimadomf  9246  nfseq  12673  seqof2  12721  rlim2  14075  nfsum1  14268  nfsum  14269  sumeq2ii  14271  fsumrelem  14380  o1fsum  14386  nfcprod1  14479  nfcprod  14480  fprodefsum  14664  prdsbas3  15964  prdsdsval2  15967  yonedalem4b  16739  gsum2d2lem  18195  coe1fzgsumdlem  19492  evl1gsumdlem  19541  ptcldmpt  21227  ptcnp  21235  cnmpt11  21276  cnmpt21  21284  cnmptk2  21299  prdsdsf  21982  prdsxmet  21984  ovolfiniun  23076  ovoliunlem3  23079  ovoliun  23080  ovoliun2  23081  ovoliunnul  23082  volfiniun  23122  voliun  23129  mbfsup  23237  mbflim  23241  itg2splitlem  23321  itg2split  23322  itg2cnlem1  23334  isibl2  23339  nfitg1  23346  nfitg  23347  cbvitg  23348  itgabs  23407  dvlipcn  23561  lhop2  23582  dvfsumabs  23590  dvfsumrlim  23598  itgparts  23614  itgsubstlem  23615  ulmss  23955  itgulm2  23967  lgamgulmlem2  24556  lgamgulmlem6  24560  lgamgulm2  24562  lgseisenlem2  24901  dchrisumlem3  24980  cnlnadjlem5  28314  dfimafnf  28817  esumfzf  29458  voliune  29619  volfiniune  29620  bnj1534  30177  bnj1542  30181  bnj958  30264  bnj1000  30265  bnj1446  30367  bnj1447  30368  bnj1448  30369  bnj1466  30375  bnj1467  30376  bnj1519  30387  bnj1520  30388  bnj1529  30392  cvmcov  30499  trpredlem1  30971  trpredrec  30982  sltval2  31053  nobndlem5  31095  finxpreclem2  32403  finxpreclem6  32409  poimirlem23  32602  poimirlem27  32606  itgabsnc  32649  riotaocN  33514  cdleme32d  34750  cdleme32f  34752  ltrniotaval  34887  cdlemksv2  35153  cdlemkuv2  35173  cdlemk36  35219  cdlemk38  35221  cdlemk19x  35249  cdlemk11t  35252  mzpsubst  36329  aomclem8  36649  binomcxplemdvbinom  37574  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  evth2f  38197  fvelrnbf  38200  evthf  38209  rfcnpre3  38215  rfcnpre4  38216  rfcnnnub  38218  refsum2cnlem1  38219  dffo3f  38359  fmul01  38647  fmuldfeqlem1  38649  fmuldfeq  38650  fmul01lt1lem1  38651  fmul01lt1lem2  38652  fmul01lt1  38653  cncfmptss  38654  mulc1cncfg  38656  expcnfg  38658  fprodabs2  38662  climmulf  38671  climexp  38672  climsuse  38675  climrecf  38676  climinff  38678  climaddf  38682  mullimc  38683  idlimc  38693  limcperiod  38695  neglimc  38714  addlimc  38715  0ellimcdiv  38716  fnlimfv  38730  climreclf  38731  fnlimcnv  38734  fnlimfvre  38741  fnlimfvre2  38744  fnlimf  38745  fnlimabslt  38746  cncfshift  38759  icccncfext  38773  cncficcgt0  38774  cncfiooicclem1  38779  dvnmul  38833  dvnprodlem1  38836  itgsubsticclem  38867  stoweidlem3  38896  stoweidlem23  38916  stoweidlem26  38919  stoweidlem28  38921  stoweidlem29  38922  stoweidlem31  38924  stoweidlem34  38927  stoweidlem36  38929  stoweidlem42  38935  stoweidlem48  38941  stoweidlem51  38944  stoweidlem52  38945  stoweidlem59  38952  wallispilem5  38962  stirlinglem4  38970  stirlinglem11  38977  stirlinglem12  38978  stirlinglem13  38979  stirlinglem14  38980  stirlinglem15  38981  fourierdlem20  39020  fourierdlem31  39031  fourierdlem79  39078  fourierdlem89  39088  fourierdlem91  39090  fourierdlem112  39111  fourierdlem115  39114  fourierd  39115  fourierclimd  39116  etransclem2  39129  etransclem48  39175  sge0revalmpt  39271  sge0fsummpt  39283  sge0iunmptlemfi  39306  sge0iunmptlemre  39308  sge0iunmpt  39311  sge0xadd  39328  sge0fsummptf  39329  sge0gtfsumgt  39336  iundjiun  39353  meadjiun  39359  voliunsge0lem  39365  omeiunle  39407  omeiunltfirp  39409  ovncvrrp  39454  vonioo  39573  vonicc  39576  vonn0ioo2  39581  vonn0icc2  39583  pimltmnf2  39588  pimgtpnf2  39594  pimltpnf2  39600  pimgtmnf2  39601  pimdecfgtioc  39602  issmff  39620  smfpimltxrmpt  39645  smfpreimagtf  39654  smflim  39663  smfpimgtxr  39666  smfpimgtxrmpt  39670  smfmullem4  39679  nfafv  39865  nfsetrecs  42232  setrec2fun  42238