This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )