Theorem nffv 5609

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 5298	. 2 |- ( F ` A ) = ( iota y A F y )
2		nffv.2	. . . 4 |- F/_ x A
3		nffv.1	. . . 4 |- F/_ x F
4		nfcv 2350	. . . 4 |- F/_ x y
5	2, 3, 4	nfbr 4106	. . 3 |- F/ x A F y
6	5	nfiotaw 5255	. 2 |- F/_ x ( iota y A F y )
7	1, 6	nfcxfr 2347	1 |- F/_ x ( F ` A )

Syntax hints:   F/_wnfc 2337   class class class wbr 4059   iotacio 5249   ` cfv 5290

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 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298

This theorem is referenced by:  nffvmpt1  5610  nffvd  5611  dffn5imf  5657  fvmptssdm  5687  fvmptf  5695  eqfnfv2f  5704  ralrnmpt  5745  rexrnmpt  5746  ffnfvf  5762  funiunfvdmf  5856  dff13f  5862  nfiso  5898  nfrecs  6416  nffrec  6505  cc2  7414  nfseq  10639  seq3f1olemstep  10696  seq3f1olemp  10697  nfsum1  11782  nfsum  11783  fsumrelem  11897  nfcprod1  11980  nfcprod  11981  ctiunctlemfo  12925  ctiunct  12926  prdsbas3  13234  cnmpt11  14870  cnmpt21  14878  lgseisenlem2  15663