Metamath Proof Explorer


Theorem ffs2

Description: Rewrite a function's support based with its range rather than the universal class. See also frnsuppeq . (Contributed by Thierry Arnoux, 27-Aug-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypothesis ffs2.1 C = B Z
Assertion ffs2 A V Z W F : A B F supp Z = F -1 C

Proof

Step Hyp Ref Expression
1 ffs2.1 C = B Z
2 frnsuppeq A V Z W F : A B F supp Z = F -1 B Z
3 2 3impia A V Z W F : A B F supp Z = F -1 B Z
4 1 imaeq2i F -1 C = F -1 B Z
5 3 4 eqtr4di A V Z W F : A B F supp Z = F -1 C