Theorem ffs2

Description: Rewrite a function's support based with its codomain rather than the universal class. See also fsuppeq . (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 e. V /\ Z e. W /\ F : A --> B ) -> ( F supp Z ) = ( `' F " C ) )

Proof

Step	Hyp	Ref	Expression
1		ffs2.1	|- C = ( B \ { Z } )
2		fsuppeq	|- ( ( A e. V /\ Z e. W ) -> ( F : A --> B -> ( F supp Z ) = ( `' F " ( B \ { Z } ) ) ) )
3	2	3impia	|- ( ( A e. V /\ Z e. W /\ F : A --> B ) -> ( F supp Z ) = ( `' F " ( B \ { Z } ) ) )
4	1	imaeq2i	|- ( `' F " C ) = ( `' F " ( B \ { Z } ) )
5	3 4	eqtr4di	|- ( ( A e. V /\ Z e. W /\ F : A --> B ) -> ( F supp Z ) = ( `' F " C ) )