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 -1 ran ⁡ F ∩ A = F -1 A

Proof

Step Hyp Ref Expression
1 inpreima ⊢ Fun ⁡ F → F -1 ran ⁡ F ∩ A = F -1 ran ⁡ F ∩ F -1 A
2 cnvimass ⊢ F -1 A ⊆ dom ⁡ F
3 cnvimarndm ⊢ F -1 ran ⁡ F = dom ⁡ F
4 2 3 sseqtrri ⊢ F -1 A ⊆ F -1 ran ⁡ F
5 dfss2 ⊢ F -1 A ⊆ F -1 ran ⁡ F ↔ F -1 A ∩ F -1 ran ⁡ F = F -1 A
6 4 5 mpbi ⊢ F -1 A ∩ F -1 ran ⁡ F = F -1 A
7 6 ineqcomi ⊢ F -1 ran ⁡ F ∩ F -1 A = F -1 A
8 1 7 eqtrdi ⊢ Fun ⁡ F → F -1 ran ⁡ F ∩ A = F -1 A