Description: Bound-variable hypothesis builder for function value. (Contributed by NM, 14-Nov-1995) (Revised by Mario Carneiro, 15-Oct-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nffv.1 | |- F/_ x F |
|
| nffv.2 | |- F/_ x A |
||
| Assertion | nffv | |- F/_ x ( F ` A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nffv.1 | |- F/_ x F |
|
| 2 | nffv.2 | |- F/_ x A |
|
| 3 | df-fv | |- ( F ` A ) = ( iota y A F y ) |
|
| 4 | nfcv | |- F/_ x y |
|
| 5 | 2 1 4 | nfbr | |- F/ x A F y |
| 6 | 5 | nfiotaw | |- F/_ x ( iota y A F y ) |
| 7 | 3 6 | nfcxfr | |- F/_ x ( F ` A ) |