Theorem nffv 6930

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

Syntax hints:  Ⅎwnfc 2893   class class class wbr 5166  ℩cio 6523  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581

This theorem is referenced by:  nffvmpt1  6931  nffvd  6932  fvelimad  6989  dffn5f  6993  fvmptss  7041  fvmptex  7043  fvmptf  7050  fvmptnf  7051  eqfnfv2f  7068  ralrnmptw  7128  ralrnmpt  7130  dffo3f  7140  ffnfvf  7154  funiunfvf  7286  dff13f  7293  nfiso  7358  nfwrecsOLD  8358  nfrdg  8470  rdgsucmptf  8484  rdgsucmptnf  8485  frsucmpt  8494  frsucmptn  8495  ttrclselem1  9794  ttrclselem2  9795  rankidb  9869  rankval4  9936  dfac8clem  10101  cardaleph  10158  hsmexlem2  10496  axcc2  10506  uniimadomf  10614  nfseq  14062  seqof2  14111  rlim2  15542  nfsum1  15738  nfsum  15739  sumeq2ii  15741  fsumrelem  15855  o1fsum  15861  nfcprod1  15956  nfcprod  15957  fprodefsum  16143  prdsbas3  17541  prdsdsval2  17544  yonedalem4b  18346  gsum2d2lem  20015  coe1fzgsumdlem  22328  evl1gsumdlem  22381  ptcldmpt  23643  ptcnp  23651  cnmpt11  23692  cnmpt21  23700  cnmptk2  23715  prdsdsf  24398  prdsxmet  24400  ovolfiniun  25555  ovoliunlem3  25558  ovoliun  25559  ovoliun2  25560  ovoliunnul  25561  volfiniun  25601  voliun  25608  mbfsup  25718  mbflim  25722  itg2splitlem  25803  itg2split  25804  itg2cnlem1  25816  isibl2  25821  nfitg1  25829  nfitg  25830  cbvitg  25831  itgabs  25890  dvlipcn  26053  lhop2  26074  dvfsumabs  26083  dvfsumrlim  26092  itgparts  26108  itgsubstlem  26109  ulmss  26458  itgulm2  26470  lgamgulmlem2  27091  lgamgulmlem6  27095  lgamgulm2  27097  lgseisenlem2  27438  dchrisumlem3  27553  sltval2  27719  nfseqs  28311  cnlnadjlem5  32103  dfimafnf  32655  2ndresdju  32667  esumfzf  34033  voliune  34193  volfiniune  34194  bnj1534  34829  bnj1542  34833  bnj958  34916  bnj1000  34917  bnj1446  35021  bnj1447  35022  bnj1448  35023  bnj1466  35029  bnj1467  35030  bnj1519  35041  bnj1520  35042  bnj1529  35046  cvmcov  35231  rdgssun  37344  exrecfnlem  37345  finxpreclem2  37356  finxpreclem6  37362  poimirlem23  37603  poimirlem27  37607  itgabsnc  37649  riotaocN  39165  cdleme32d  40401  cdleme32f  40403  ltrniotaval  40538  cdlemksv2  40804  cdlemkuv2  40824  cdlemk36  40870  cdlemk38  40872  cdlemk19x  40900  cdlemk11t  40903  evl1gprodd  42074  mzpsubst  42704  aomclem8  43018  mnringmulrcld  44197  binomcxplemdvbinom  44322  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  evth2f  44915  fvelrnbf  44918  evthf  44927  rfcnpre3  44933  rfcnpre4  44934  rfcnnnub  44936  refsum2cnlem1  44937  allbutfiinf  45335  monoordxr  45398  monoord2xr  45400  caucvgbf  45405  cvgcaule  45407  fmul01  45501  fmuldfeqlem1  45503  fmuldfeq  45504  fmul01lt1lem1  45505  fmul01lt1lem2  45506  fmul01lt1  45507  cncfmptss  45508  mulc1cncfg  45510  expcnfg  45512  fprodabs2  45516  climmulf  45525  climexp  45526  climsuse  45529  climrecf  45530  climinff  45532  climaddf  45536  mullimc  45537  idlimc  45547  limcperiod  45549  neglimc  45568  addlimc  45569  0ellimcdiv  45570  fnlimfv  45584  climreclf  45585  fnlimcnv  45588  fnlimfvre  45595  fnlimfvre2  45598  fnlimf  45599  fnlimabslt  45600  climfveqf  45601  climmptf  45602  climeldmeqf  45604  limsupref  45606  limsupbnd1f  45607  climbddf  45608  climeqf  45609  limsuppnfd  45623  climinf2  45628  limsuppnf  45632  limsupubuz  45634  climinfmpt  45636  limsupmnf  45642  limsupequz  45644  limsupre2  45646  limsupmnfuz  45648  limsupre3  45654  limsupre3uz  45657  limsupreuz  45658  climuz  45665  lmbr3  45668  limsupgt  45699  liminfvalxr  45704  liminfreuz  45724  liminflt  45726  xlimpnfxnegmnf  45735  liminfpnfuz  45737  xlimmnf  45762  xlimpnf  45763  dfxlim2  45769  xlimpnfxnegmnf2  45779  cncfshift  45795  icccncfext  45808  cncficcgt0  45809  cncfiooicclem1  45814  dvnmul  45864  dvnprodlem1  45867  itgsubsticclem  45896  stoweidlem3  45924  stoweidlem23  45944  stoweidlem26  45947  stoweidlem28  45949  stoweidlem29  45950  stoweidlem31  45952  stoweidlem34  45955  stoweidlem36  45957  stoweidlem42  45963  stoweidlem48  45969  stoweidlem51  45972  stoweidlem52  45973  stoweidlem59  45980  wallispilem5  45990  stirlinglem4  45998  stirlinglem11  46005  stirlinglem12  46006  stirlinglem13  46007  stirlinglem14  46008  stirlinglem15  46009  fourierdlem20  46048  fourierdlem31  46059  fourierdlem79  46106  fourierdlem89  46116  fourierdlem91  46118  fourierdlem112  46139  fourierdlem115  46142  fourierd  46143  fourierclimd  46144  etransclem2  46157  etransclem48  46203  sge0revalmpt  46299  sge0fsummpt  46311  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  sge0iunmpt  46339  sge0xadd  46356  sge0fsummptf  46357  sge0gtfsumgt  46364  iundjiun  46381  meadjiun  46387  voliunsge0lem  46393  meaiunincf  46404  meaiuninc3  46406  omeiunle  46438  omeiunltfirp  46440  ovncvrrp  46485  vonioo  46603  vonicc  46606  vonn0ioo2  46611  vonn0icc2  46613  pimltmnf2f  46618  pimgtpnf2f  46626  pimltpnf2f  46633  pimgtmnf2  46635  pimdecfgtioc  46636  issmff  46655  smfpimltxrmptf  46679  smfpreimagtf  46689  smflim  46698  smfpimgtxr  46701  smfpimgtxrmptf  46705  smfmullem4  46715  smflim2  46727  smfpimcclem  46728  smfpimcc  46729  smfsup  46735  smfsupmpt  46736  smfsupxr  46737  smfinflem  46738  smfinf  46739  smfinfmpt  46740  smflimsuplem2  46742  smflimsuplem5  46745  smflimsuplem7  46747  smflimsup  46749  smfliminf  46752  fsupdm  46763  smfsupdmmbllem  46765  finfdm  46767  smfinfdmmbllem  46769  nfafv  47051  nfsetrecs  48778  setrec2fun  48784