Metamath Proof Explorer


Theorem fvimacnvi

Description: A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007)

Ref Expression
Assertion fvimacnvi Fun F A F -1 B F A B

Proof

Step Hyp Ref Expression
1 snssi A F -1 B A F -1 B
2 funimass2 Fun F A F -1 B F A B
3 1 2 sylan2 Fun F A F -1 B F A B
4 fvex F A V
5 4 snss F A B F A B
6 cnvimass F -1 B dom F
7 6 sseli A F -1 B A dom F
8 funfn Fun F F Fn dom F
9 fnsnfv F Fn dom F A dom F F A = F A
10 8 9 sylanb Fun F A dom F F A = F A
11 7 10 sylan2 Fun F A F -1 B F A = F A
12 11 sseq1d Fun F A F -1 B F A B F A B
13 5 12 syl5bb Fun F A F -1 B F A B F A B
14 3 13 mpbird Fun F A F -1 B F A B