Metamath Proof Explorer


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 FunFranFBF-1A=F-1AB

Proof

Step Hyp Ref Expression
1 inass ABranF=ABranF
2 sseqin2 ranFBBranF=ranF
3 2 biimpi ranFBBranF=ranF
4 3 adantl FunFranFBBranF=ranF
5 4 ineq2d FunFranFBABranF=AranF
6 1 5 eqtrid FunFranFBABranF=AranF
7 6 imaeq2d FunFranFBF-1ABranF=F-1AranF
8 fimacnvinrn FunFF-1AB=F-1ABranF
9 8 adantr FunFranFBF-1AB=F-1ABranF
10 fimacnvinrn FunFF-1A=F-1AranF
11 10 adantr FunFranFBF-1A=F-1AranF
12 7 9 11 3eqtr4rd FunFranFBF-1A=F-1AB