Theorem nffv 5598

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	|- F/_ x F
nffv.2	|- F/_ x A

Assertion

Ref	Expression
nffv	|- F/_ x ( F ` A )

Proof of Theorem nffv

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-fv 5287	. 2 |- ( F ` A ) = ( iota y A F y )
2		nffv.2	. . . 4 |- F/_ x A
3		nffv.1	. . . 4 |- F/_ x F
4		nfcv 2349	. . . 4 |- F/_ x y
5	2, 3, 4	nfbr 4097	. . 3 |- F/ x A F y
6	5	nfiotaw 5244	. 2 |- F/_ x ( iota y A F y )
7	1, 6	nfcxfr 2346	1 |- F/_ x ( F ` A )

Syntax hints:   F/_wnfc 2336   class class class wbr 4050   iotacio 5238   ` cfv 5279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491  df-v 2775  df-un 3174  df-sn 3643  df-pr 3644  df-op 3646  df-uni 3856  df-br 4051  df-iota 5240  df-fv 5287

This theorem is referenced by:  nffvmpt1  5599  nffvd  5600  dffn5imf  5646  fvmptssdm  5676  fvmptf  5684  eqfnfv2f  5693  ralrnmpt  5734  rexrnmpt  5735  ffnfvf  5751  funiunfvdmf  5845  dff13f  5851  nfiso  5887  nfrecs  6405  nffrec  6494  cc2  7394  nfseq  10619  seq3f1olemstep  10676  seq3f1olemp  10677  nfsum1  11737  nfsum  11738  fsumrelem  11852  nfcprod1  11935  nfcprod  11936  ctiunctlemfo  12880  ctiunct  12881  prdsbas3  13189  cnmpt11  14825  cnmpt21  14833  lgseisenlem2  15618