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 ( ( 𝐹 ''' 𝐴 ) ∈ 𝐵 → ( 𝐹 ''' 𝐴 ) = ( 𝐹𝐴 ) )

Proof

Step Hyp Ref Expression
1 nvelim ( ( 𝐹 ''' 𝐴 ) = V → ¬ ( 𝐹 ''' 𝐴 ) ∈ 𝐵 )
2 1 necon2ai ( ( 𝐹 ''' 𝐴 ) ∈ 𝐵 → ( 𝐹 ''' 𝐴 ) ≠ V )
3 afvnufveq ( ( 𝐹 ''' 𝐴 ) ≠ V → ( 𝐹 ''' 𝐴 ) = ( 𝐹𝐴 ) )
4 2 3 syl ( ( 𝐹 ''' 𝐴 ) ∈ 𝐵 → ( 𝐹 ''' 𝐴 ) = ( 𝐹𝐴 ) )