Theorem cnvimainrn

Description: The preimage of the intersection of the range of a class and a class A is the preimage of the class A . (Contributed by AV, 17-Sep-2024)

	Ref	Expression
Assertion	cnvimainrn	|- ( Fun F -> ( `' F " ( ran F i^i A ) ) = ( `' F " A ) )

Proof

Step	Hyp	Ref	Expression
1		inpreima	|- ( Fun F -> ( `' F " ( ran F i^i A ) ) = ( ( `' F " ran F ) i^i ( `' F " A ) ) )
2		cnvimass	|- ( `' F " A ) C_ dom F
3		cnvimarndm	|- ( `' F " ran F ) = dom F
4	2 3	sseqtrri	|- ( `' F " A ) C_ ( `' F " ran F )
5		dfss2	|- ( ( `' F " A ) C_ ( `' F " ran F ) <-> ( ( `' F " A ) i^i ( `' F " ran F ) ) = ( `' F " A ) )
6	4 5	mpbi	|- ( ( `' F " A ) i^i ( `' F " ran F ) ) = ( `' F " A )
7	6	ineqcomi	|- ( ( `' F " ran F ) i^i ( `' F " A ) ) = ( `' F " A )
8	1 7	eqtrdi	|- ( Fun F -> ( `' F " ( ran F i^i A ) ) = ( `' F " A ) )