Description: If a function is defined at a class A the alternate function value at A is the unique value assigned to A by the function (analogously to ( FA ) ). (Contributed by AV, 2-Sep-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dfatafv2iota | |- ( F defAt A -> ( F '''' A ) = ( iota x A F x ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-afv2 | |- ( F '''' A ) = if ( F defAt A , ( iota x A F x ) , ~P U. ran F ) |
|
| 2 | iftrue | |- ( F defAt A -> if ( F defAt A , ( iota x A F x ) , ~P U. ran F ) = ( iota x A F x ) ) |
|
| 3 | 1 2 | syl5eq | |- ( F defAt A -> ( F '''' A ) = ( iota x A F x ) ) |