Metamath Proof Explorer


Theorem funressndmfvrn

Description: The value of a function F at a set A is in the range of the function F if A is in the domain of the function F . It is sufficient that F is a function at A . (Contributed by AV, 1-Sep-2022)

Ref Expression
Assertion funressndmfvrn Fun F A A dom F F A ran F

Proof

Step Hyp Ref Expression
1 simpr Fun F A A dom F A dom F
2 fvressn A dom F F A A = F A
3 2 adantl Fun F A A dom F F A A = F A
4 eldmressnsn A dom F A dom F A
5 fvelrn Fun F A A dom F A F A A ran F A
6 4 5 sylan2 Fun F A A dom F F A A ran F A
7 3 6 eqeltrrd Fun F A A dom F F A ran F A
8 fvrnressn A dom F F A ran F A F A ran F
9 1 7 8 sylc Fun F A A dom F F A ran F