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 𝐹 → ( ◡ 𝐹 “ ( ran 𝐹 ∩ 𝐴 ) ) = ( ◡ 𝐹 “ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		inpreima	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( ran 𝐹 ∩ 𝐴 ) ) = ( ( ◡ 𝐹 “ ran 𝐹 ) ∩ ( ◡ 𝐹 “ 𝐴 ) ) )
2		cnvimass	⊢ ( ◡ 𝐹 “ 𝐴 ) ⊆ dom 𝐹
3		cnvimarndm	⊢ ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹
4	2 3	sseqtrri	⊢ ( ◡ 𝐹 “ 𝐴 ) ⊆ ( ◡ 𝐹 “ ran 𝐹 )
5		dfss2	⊢ ( ( ◡ 𝐹 “ 𝐴 ) ⊆ ( ◡ 𝐹 “ ran 𝐹 ) ↔ ( ( ◡ 𝐹 “ 𝐴 ) ∩ ( ◡ 𝐹 “ ran 𝐹 ) ) = ( ◡ 𝐹 “ 𝐴 ) )
6	4 5	mpbi	⊢ ( ( ◡ 𝐹 “ 𝐴 ) ∩ ( ◡ 𝐹 “ ran 𝐹 ) ) = ( ◡ 𝐹 “ 𝐴 )
7	6	ineqcomi	⊢ ( ( ◡ 𝐹 “ ran 𝐹 ) ∩ ( ◡ 𝐹 “ 𝐴 ) ) = ( ◡ 𝐹 “ 𝐴 )
8	1 7	eqtrdi	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( ran 𝐹 ∩ 𝐴 ) ) = ( ◡ 𝐹 “ 𝐴 ) )