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 | ⊢ ( ( 𝐹 ''' 𝐴 ) ∈ 𝐵 → ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nvelim | ⊢ ( ( 𝐹 ''' 𝐴 ) = V → ¬ ( 𝐹 ''' 𝐴 ) ∈ 𝐵 ) | |
2 | 1 | necon2ai | ⊢ ( ( 𝐹 ''' 𝐴 ) ∈ 𝐵 → ( 𝐹 ''' 𝐴 ) ≠ V ) |
3 | afvnufveq | ⊢ ( ( 𝐹 ''' 𝐴 ) ≠ V → ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ) | |
4 | 2 3 | syl | ⊢ ( ( 𝐹 ''' 𝐴 ) ∈ 𝐵 → ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ) |