Theorem nffv 6832

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 6489	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		nffv.2	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nffv.1	. . . 4 ⊢ Ⅎ𝑥𝐹
4		nfcv 2894	. . . 4 ⊢ Ⅎ𝑥𝑦
5	2, 3, 4	nfbr 5136	. . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦
6	5	nfiotaw 6441	. 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦)
7	1, 6	nfcxfr 2892	1 ⊢ Ⅎ𝑥(𝐹‘𝐴)

Syntax hints:  Ⅎwnfc 2879   class class class wbr 5089  ℩cio 6435  ‘cfv 6481

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489

This theorem is referenced by:  nffvmpt1  6833  nffvd  6834  fvelimad  6889  dffn5f  6893  fvmptss  6941  fvmptex  6943  fvmptf  6950  fvmptnf  6951  eqfnfv2f  6968  ralrnmptw  7027  ralrnmpt  7029  dffo3f  7039  ffnfvf  7053  funiunfvf  7183  dff13f  7189  nfiso  7256  nfrdg  8333  rdgsucmptf  8347  rdgsucmptnf  8348  frsucmpt  8357  frsucmptn  8358  ttrclselem1  9615  ttrclselem2  9616  rankidb  9693  rankval4  9760  dfac8clem  9923  cardaleph  9980  hsmexlem2  10318  axcc2  10328  uniimadomf  10436  nfseq  13918  seqof2  13967  rlim2  15403  nfsum1  15597  nfsum  15598  sumeq2ii  15600  fsumrelem  15714  o1fsum  15720  nfcprod1  15815  nfcprod  15816  fprodefsum  16002  prdsbas3  17385  prdsdsval2  17388  yonedalem4b  18182  gsum2d2lem  19885  coe1fzgsumdlem  22218  evl1gsumdlem  22271  ptcldmpt  23529  ptcnp  23537  cnmpt11  23578  cnmpt21  23586  cnmptk2  23601  prdsdsf  24282  prdsxmet  24284  ovolfiniun  25429  ovoliunlem3  25432  ovoliun  25433  ovoliun2  25434  ovoliunnul  25435  volfiniun  25475  voliun  25482  mbfsup  25592  mbflim  25596  itg2splitlem  25676  itg2split  25677  itg2cnlem1  25689  isibl2  25694  nfitg1  25702  nfitg  25703  cbvitg  25704  itgabs  25763  dvlipcn  25926  lhop2  25947  dvfsumabs  25956  dvfsumrlim  25965  itgparts  25981  itgsubstlem  25982  ulmss  26333  itgulm2  26345  lgamgulmlem2  26967  lgamgulmlem6  26971  lgamgulm2  26973  lgseisenlem2  27314  dchrisumlem3  27429  sltval2  27595  nfseqs  28217  cnlnadjlem5  32051  dfimafnf  32618  2ndresdju  32631  esumfzf  34082  voliune  34242  volfiniune  34243  bnj1534  34865  bnj1542  34869  bnj958  34952  bnj1000  34953  bnj1446  35057  bnj1447  35058  bnj1448  35059  bnj1466  35065  bnj1467  35066  bnj1519  35077  bnj1520  35078  bnj1529  35082  rankval4b  35111  onvf1odlem2  35148  cvmcov  35307  rdgssun  37422  exrecfnlem  37423  finxpreclem2  37434  finxpreclem6  37440  poimirlem23  37682  poimirlem27  37686  itgabsnc  37728  riotaocN  39307  cdleme32d  40542  cdleme32f  40544  ltrniotaval  40679  cdlemksv2  40945  cdlemkuv2  40965  cdlemk36  41011  cdlemk38  41013  cdlemk19x  41041  cdlemk11t  41044  evl1gprodd  42209  mzpsubst  42840  aomclem8  43153  mnringmulrcld  44320  binomcxplemdvbinom  44445  binomcxplemdvsum  44447  binomcxplemnotnn0  44448  nfrelp  45041  permaxrep  45098  permaxsep  45099  evth2f  45111  fvelrnbf  45114  evthf  45123  rfcnpre3  45129  rfcnpre4  45130  rfcnnnub  45132  refsum2cnlem1  45133  allbutfiinf  45517  monoordxr  45579  monoord2xr  45581  caucvgbf  45586  cvgcaule  45588  fmul01  45679  fmuldfeqlem1  45681  fmuldfeq  45682  fmul01lt1lem1  45683  fmul01lt1lem2  45684  fmul01lt1  45685  cncfmptss  45686  mulc1cncfg  45688  expcnfg  45690  fprodabs2  45694  climmulf  45703  climexp  45704  climsuse  45707  climrecf  45708  climinff  45710  climaddf  45714  mullimc  45715  idlimc  45725  limcperiod  45727  neglimc  45744  addlimc  45745  0ellimcdiv  45746  fnlimfv  45760  climreclf  45761  fnlimcnv  45764  fnlimfvre  45771  fnlimfvre2  45774  fnlimf  45775  fnlimabslt  45776  climfveqf  45777  climmptf  45778  climeldmeqf  45780  limsupref  45782  limsupbnd1f  45783  climbddf  45784  climeqf  45785  limsuppnfd  45799  climinf2  45804  limsuppnf  45808  limsupubuz  45810  climinfmpt  45812  limsupmnf  45818  limsupequz  45820  limsupre2  45822  limsupmnfuz  45824  limsupre3  45830  limsupre3uz  45833  limsupreuz  45834  climuz  45841  lmbr3  45844  limsupgt  45875  liminfvalxr  45880  liminfreuz  45900  liminflt  45902  xlimpnfxnegmnf  45911  liminfpnfuz  45913  xlimmnf  45938  xlimpnf  45939  dfxlim2  45945  xlimpnfxnegmnf2  45955  cncfshift  45971  icccncfext  45984  cncficcgt0  45985  cncfiooicclem1  45990  dvnmul  46040  dvnprodlem1  46043  itgsubsticclem  46072  stoweidlem3  46100  stoweidlem23  46120  stoweidlem26  46123  stoweidlem28  46125  stoweidlem29  46126  stoweidlem31  46128  stoweidlem34  46131  stoweidlem36  46133  stoweidlem42  46139  stoweidlem48  46145  stoweidlem51  46148  stoweidlem52  46149  stoweidlem59  46156  wallispilem5  46166  stirlinglem4  46174  stirlinglem11  46181  stirlinglem12  46182  stirlinglem13  46183  stirlinglem14  46184  stirlinglem15  46185  fourierdlem20  46224  fourierdlem31  46235  fourierdlem79  46282  fourierdlem89  46292  fourierdlem91  46294  fourierdlem112  46315  fourierdlem115  46318  fourierd  46319  fourierclimd  46320  etransclem2  46333  etransclem48  46379  sge0revalmpt  46475  sge0fsummpt  46487  sge0iunmptlemfi  46510  sge0iunmptlemre  46512  sge0iunmpt  46515  sge0xadd  46532  sge0fsummptf  46533  sge0gtfsumgt  46540  iundjiun  46557  meadjiun  46563  voliunsge0lem  46569  meaiunincf  46580  meaiuninc3  46582  omeiunle  46614  omeiunltfirp  46616  ovncvrrp  46661  vonioo  46779  vonicc  46782  vonn0ioo2  46787  vonn0icc2  46789  pimltmnf2f  46794  pimgtpnf2f  46802  pimltpnf2f  46809  pimgtmnf2  46811  pimdecfgtioc  46812  issmff  46831  smfpimltxrmptf  46855  smfpreimagtf  46865  smflim  46874  smfpimgtxr  46877  smfpimgtxrmptf  46881  smfmullem4  46891  smflim2  46903  smfpimcclem  46904  smfpimcc  46905  smfsup  46911  smfsupmpt  46912  smfsupxr  46913  smfinflem  46914  smfinf  46915  smflimsuplem2  46918  smflimsuplem5  46921  smflimsuplem7  46923  smflimsup  46925  smfliminf  46928  fsupdm  46939  smfsupdmmbllem  46941  finfdm  46943  smfinfdmmbllem  46945  nfafv  47235  nfsetrecs  49786  setrec2fun  49792