Description: Bound-variable hypothesis builder for function value, analogous to nffv . To prove a deduction version of this analogous to nffvd is not easily possible because a deduction version of nfdfat cannot be shown easily. (Contributed by AV, 4-Sep-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfafv2.1 | |- F/_ x F |
|
| nfafv2.2 | |- F/_ x A |
||
| Assertion | nfafv2 | |- F/_ x ( F '''' A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfafv2.1 | |- F/_ x F |
|
| 2 | nfafv2.2 | |- F/_ x A |
|
| 3 | df-afv2 | |- ( F '''' A ) = if ( F defAt A , ( iota y A F y ) , ~P U. ran F ) |
|
| 4 | 1 2 | nfdfat | |- F/ x F defAt A |
| 5 | nfcv | |- F/_ x y |
|
| 6 | 2 1 5 | nfbr | |- F/ x A F y |
| 7 | 6 | nfiotaw | |- F/_ x ( iota y A F y ) |
| 8 | 1 | nfrn | |- F/_ x ran F |
| 9 | 8 | nfuni | |- F/_ x U. ran F |
| 10 | 9 | nfpw | |- F/_ x ~P U. ran F |
| 11 | 4 7 10 | nfif | |- F/_ x if ( F defAt A , ( iota y A F y ) , ~P U. ran F ) |
| 12 | 3 11 | nfcxfr | |- F/_ x ( F '''' A ) |