Theorem dfatafv2eqfv

Description: If a function is defined at a class A , the alternate function value equals the function's value at A . (Contributed by AV, 3-Sep-2022)

	Ref	Expression
Assertion	dfatafv2eqfv	|- ( F defAt A -> ( F '''' A ) = ( F ` A ) )

Proof

Step	Hyp	Ref	Expression
1		dfafv22	|- ( F '''' A ) = if ( F defAt A , ( F ` A ) , ~P U. ran F )
2		iftrue	|- ( F defAt A -> if ( F defAt A , ( F ` A ) , ~P U. ran F ) = ( F ` A ) )
3	1 2	syl5eq	|- ( F defAt A -> ( F '''' A ) = ( F ` A ) )