Metamath Proof Explorer


Theorem afvvfveq

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 B F ''' A = F A

Proof

Step Hyp Ref Expression
1 nvelim F ''' A = V ¬ F ''' A B
2 1 necon2ai F ''' A B F ''' A V
3 afvnufveq F ''' A V F ''' A = F A
4 2 3 syl F ''' A B F ''' A = F A