Metamath Proof Explorer


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 𝒫 ran F
2 iftrue F defAt A if F defAt A F A 𝒫 ran F = F A
3 1 2 eqtrid F defAt A F '''' A = F A