Theorem nffv 6900

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 6551	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2922	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5151	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6501	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2920	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

This proof depends on syntax axioms:  Ⅎwnfc 2907   class class class wbr 5102  ℩cio 6495  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551

This theorem is used by:  nffvmpt1  6901  nffvd  6902  fvelimad  6957  dffn5f  6961  fvmptss  7011  fvmptex  7013  fvmptf  7020  fvmptnf  7021  eqfnfv2f  7038  ralrnmptw  7099  ralrnmpt  7101  dffo3f  7111  ffnfvf  7125  funiunfvf  7257  dff13f  7263  nfiso  7334  nfrdg  8429  rdgsucmptf  8443  rdgsucmptnf  8444  frsucmpt  8453  frsucmptn  8454  ttrclselem1  9733  ttrclselem2  9734  rankidb  9815  rankval4b  9887  rankval4  9891  setrec2fun  9980  dfac8clem  10118  cardaleph  10175  hsmexlem2  10512  axcc2  10522  uniimadomf  10636  nfseq  14161  seqof2  14210  rlim2  15672  nfsum1  15866  nfsum  15867  sumeq2ii  15869  fsumrelem  15983  o1fsum  15989  nfcprod1  16086  nfcprod  16087  fprodefsum  16270  prdsbas3  17661  prdsdsval2  17664  yonedalem4b  18459  gsum2d2lem  20196  coe1fzgsumdlem  22630  evl1gsumdlem  22683  ptcldmpt  23942  ptcnp  23950  cnmpt11  23991  cnmpt21  23999  cnmptk2  24014  prdsdsf  24695  prdsxmet  24697  ovolfiniun  25831  ovoliunlem3  25834  ovoliun  25835  ovoliun2  25836  ovoliunnul  25837  volfiniun  25877  voliun  25884  mbfsup  25994  mbflim  25998  itg2splitlem  26078  itg2split  26079  itg2cnlem1  26091  isibl2  26096  nfitg1  26103  nfitg  26104  cbvitg  26105  itgabs  26164  dvlipcn  26323  lhop2  26344  dvfsumabs  26352  dvfsumrlim  26360  itgparts  26376  itgsubstlem  26377  ulmss  26733  itgulm2  26745  lgamgulmlem2  27366  lgamgulmlem6  27370  lgamgulm2  27372  lgseisenlem2  27712  dchrisumlem3  27827  ltsval2  28022  nfseqs  28682  cnlnadjlem5  32682  dfimafnf  33281  2ndresdju  33294  deg1prod  34165  esumfzf  34751  voliune  34912  volfiniune  34913  bnj1534  35533  bnj1542  35537  bnj958  35620  bnj1000  35621  bnj1446  35725  bnj1447  35726  bnj1448  35727  bnj1466  35733  bnj1467  35734  bnj1519  35745  bnj1520  35746  bnj1529  35750  onvf1odlem2  35955  onprcf1acwevdlem2  35969  vonf1oonfo  35972  onprcf1of1ord  35978  srepdflem1  36008  cvmcov  36118  rdgssun  38410  exrecfnlem  38411  finxpreclem2  38422  finxpreclem6  38428  poimirlem23  38670  poimirlem27  38674  itgabsnc  38716  riotaocN  40375  cdleme32d  41610  cdleme32f  41612  ltrniotaval  41747  cdlemksv2  42013  cdlemkuv2  42033  cdlemk36  42079  cdlemk38  42081  cdlemk19x  42109  cdlemk11t  42112  evl1gprodd  43276  mzpsubst  43868  aomclem8  44172  mnringmulrcld  45335  binomcxplemdvbinom  45446  binomcxplemdvsum  45448  binomcxplemnotnn0  45449  nfrelp  46047  permaxrep  46104  permaxsep  46105  evth2f  46140  fvelrnbf  46143  evthf  46152  rfcnpre3  46158  rfcnpre4  46159  rfcnnnub  46161  refsum2cnlem1  46162  allbutfiinf  46538  monoordxr  46600  monoord2xr  46602  caucvgbf  46607  cvgcaule  46609  fmul01  46700  fmuldfeqlem1  46702  fmuldfeq  46703  fmul01lt1lem1  46704  fmul01lt1lem2  46705  fmul01lt1  46706  cncfmptss  46707  mulc1cncfg  46709  expcnfg  46711  fprodabs2  46715  climmulf  46724  climexp  46725  climsuse  46728  climrecf  46729  climinff  46731  climaddf  46735  mullimc  46736  idlimc  46746  limcperiod  46748  neglimc  46765  addlimc  46766  0ellimcdiv  46767  fnlimfv  46781  climreclf  46782  fnlimcnv  46785  fnlimfvre  46792  fnlimfvre2  46795  fnlimf  46796  fnlimabslt  46797  climfveqf  46798  climmptf  46799  climeldmeqf  46801  limsupref  46803  limsupbnd1f  46804  climbddf  46805  climeqf  46806  limsuppnfd  46820  climinf2  46825  limsuppnf  46829  limsupubuz  46831  climinfmpt  46833  limsupmnf  46839  limsupequz  46841  limsupre2  46843  limsupmnfuz  46845  limsupre3  46851  limsupre3uz  46854  limsupreuz  46855  climuz  46862  lmbr3  46865  limsupgt  46896  liminfvalxr  46901  liminfreuz  46921  liminflt  46923  xlimpnfxnegmnf  46932  liminfpnfuz  46934  xlimmnf  46959  xlimpnf  46960  dfxlim2  46966  xlimpnfxnegmnf2  46976  cncfshift  46992  icccncfext  47005  cncficcgt0  47006  cncfiooicclem1  47011  dvnmul  47061  dvnprodlem1  47064  itgsubsticclem  47093  stoweidlem3  47121  stoweidlem23  47141  stoweidlem26  47144  stoweidlem28  47146  stoweidlem29  47147  stoweidlem31  47149  stoweidlem34  47152  stoweidlem36  47154  stoweidlem42  47160  stoweidlem48  47166  stoweidlem51  47169  stoweidlem52  47170  stoweidlem59  47177  wallispilem5  47187  stirlinglem4  47195  stirlinglem11  47202  stirlinglem12  47203  stirlinglem13  47204  stirlinglem14  47205  stirlinglem15  47206  fourierdlem20  47245  fourierdlem31  47256  fourierdlem79  47303  fourierdlem89  47313  fourierdlem91  47315  fourierdlem112  47336  fourierdlem115  47339  fourierd  47340  fourierclimd  47341  etransclem2  47354  etransclem48  47400  sge0revalmpt  47496  sge0fsummpt  47508  sge0iunmptlemfi  47531  sge0iunmptlemre  47533  sge0iunmpt  47536  sge0xadd  47553  sge0fsummptf  47554  sge0gtfsumgt  47561  iundjiun  47578  meadjiun  47584  voliunsge0lem  47590  meaiunincf  47601  meaiuninc3  47603  omeiunle  47635  omeiunltfirp  47637  ovncvrrp  47682  vonioo  47800  vonicc  47803  vonn0ioo2  47808  vonn0icc2  47810  pimltmnf2f  47815  pimgtpnf2f  47823  pimltpnf2f  47830  pimgtmnf2  47832  pimdecfgtioc  47833  issmff  47852  smfpimltxrmptf  47876  smfpreimagtf  47886  smflim  47895  smfpimgtxr  47898  smfpimgtxrmptf  47902  smfmullem4  47912  smflim2  47924  smfpimcclem  47925  smfpimcc  47926  smfsup  47932  smfsupmpt  47933  smfsupxr  47934  smfinflem  47935  smfinf  47936  smflimsuplem2  47939  smflimsuplem5  47942  smflimsuplem7  47944  smflimsup  47946  smfliminf  47949  fsupdm  47960  smfsupdmmbllem  47962  finfdm  47964  smfinfdmmbllem  47966  nfafv  48314  nfsetrecs  50972