Description: The value of the alternative function at a set as argument equals the function's value at this argument. (Contributed by Alexander van der Vekens, 25-May-2017)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | afvvfveq | |- ( ( F ''' A ) e. B -> ( F ''' A ) = ( F ` A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nvelim | |- ( ( F ''' A ) = _V -> -. ( F ''' A ) e. B ) |
|
| 2 | 1 | necon2ai | |- ( ( F ''' A ) e. B -> ( F ''' A ) =/= _V ) |
| 3 | afvnufveq | |- ( ( F ''' A ) =/= _V -> ( F ''' A ) = ( F ` A ) ) |
|
| 4 | 2 3 | syl | |- ( ( F ''' A ) e. B -> ( F ''' A ) = ( F ` A ) ) |