Metamath Proof Explorer


Theorem afv2elrn

Description: An alternate function value belongs to the range of the function, analogous to fvelrn . (Contributed by AV, 3-Sep-2022)

Ref Expression
Assertion afv2elrn Fun F A dom F F '''' A ran F

Proof

Step Hyp Ref Expression
1 fundmdfat Fun F A dom F F defAt A
2 dfatafv2rnb F defAt A F '''' A ran F
3 1 2 sylib Fun F A dom F F '''' A ran F