Theorem fimacnvinrn2

Description: Taking the converse image of a set can be limited to the range of the function used. (Contributed by Thierry Arnoux, 17-Feb-2017)

	Ref	Expression
Assertion	fimacnvinrn2	|- ( ( Fun F /\ ran F C_ B ) -> ( `' F " A ) = ( `' F " ( A i^i B ) ) )

Proof

Step	Hyp	Ref	Expression
1		inass	|- ( ( A i^i B ) i^i ran F ) = ( A i^i ( B i^i ran F ) )
2		sseqin2	|- ( ran F C_ B <-> ( B i^i ran F ) = ran F )
3	2	biimpi	|- ( ran F C_ B -> ( B i^i ran F ) = ran F )
4	3	adantl	|- ( ( Fun F /\ ran F C_ B ) -> ( B i^i ran F ) = ran F )
5	4	ineq2d	|- ( ( Fun F /\ ran F C_ B ) -> ( A i^i ( B i^i ran F ) ) = ( A i^i ran F ) )
6	1 5	syl5eq	|- ( ( Fun F /\ ran F C_ B ) -> ( ( A i^i B ) i^i ran F ) = ( A i^i ran F ) )
7	6	imaeq2d	|- ( ( Fun F /\ ran F C_ B ) -> ( `' F " ( ( A i^i B ) i^i ran F ) ) = ( `' F " ( A i^i ran F ) ) )
8		fimacnvinrn	|- ( Fun F -> ( `' F " ( A i^i B ) ) = ( `' F " ( ( A i^i B ) i^i ran F ) ) )
9	8	adantr	|- ( ( Fun F /\ ran F C_ B ) -> ( `' F " ( A i^i B ) ) = ( `' F " ( ( A i^i B ) i^i ran F ) ) )
10		fimacnvinrn	|- ( Fun F -> ( `' F " A ) = ( `' F " ( A i^i ran F ) ) )
11	10	adantr	|- ( ( Fun F /\ ran F C_ B ) -> ( `' F " A ) = ( `' F " ( A i^i ran F ) ) )
12	7 9 11	3eqtr4rd	|- ( ( Fun F /\ ran F C_ B ) -> ( `' F " A ) = ( `' F " ( A i^i B ) ) )