Metamath Proof Explorer


Theorem funfvima

Description: A function's value in a preimage belongs to the image. (Contributed by NM, 23-Sep-2003)

Ref Expression
Assertion funfvima Fun F B dom F B A F B F A

Proof

Step Hyp Ref Expression
1 dmres dom F A = A dom F
2 1 elin2 B dom F A B A B dom F
3 funres Fun F Fun F A
4 fvelrn Fun F A B dom F A F A B ran F A
5 3 4 sylan Fun F B dom F A F A B ran F A
6 df-ima F A = ran F A
7 6 eleq2i F B F A F B ran F A
8 fvres B A F A B = F B
9 8 eleq1d B A F A B ran F A F B ran F A
10 7 9 bitr4id B A F B F A F A B ran F A
11 5 10 syl5ibrcom Fun F B dom F A B A F B F A
12 11 ex Fun F B dom F A B A F B F A
13 2 12 syl5bir Fun F B A B dom F B A F B F A
14 13 expd Fun F B A B dom F B A F B F A
15 14 com12 B A Fun F B dom F B A F B F A
16 15 impd B A Fun F B dom F B A F B F A
17 16 pm2.43b Fun F B dom F B A F B F A