Theorem sspreima

Description: The preimage of a subset is a subset of the preimage. (Contributed by Brendan Leahy, 23-Sep-2017)

	Ref	Expression
Assertion	sspreima	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ 𝐵 ) → ( ◡ 𝐹 “ 𝐴 ) ⊆ ( ◡ 𝐹 “ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		inpreima	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) = ( ( ◡ 𝐹 “ 𝐴 ) ∩ ( ◡ 𝐹 “ 𝐵 ) ) )
2		dfss2	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )
3	2	biimpi	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∩ 𝐵 ) = 𝐴 )
4	3	imaeq2d	⊢ ( 𝐴 ⊆ 𝐵 → ( ◡ 𝐹 “ ( 𝐴 ∩ 𝐵 ) ) = ( ◡ 𝐹 “ 𝐴 ) )
5	1 4	sylan9req	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ 𝐵 ) → ( ( ◡ 𝐹 “ 𝐴 ) ∩ ( ◡ 𝐹 “ 𝐵 ) ) = ( ◡ 𝐹 “ 𝐴 ) )
6		dfss2	⊢ ( ( ◡ 𝐹 “ 𝐴 ) ⊆ ( ◡ 𝐹 “ 𝐵 ) ↔ ( ( ◡ 𝐹 “ 𝐴 ) ∩ ( ◡ 𝐹 “ 𝐵 ) ) = ( ◡ 𝐹 “ 𝐴 ) )
7	5 6	sylibr	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ 𝐵 ) → ( ◡ 𝐹 “ 𝐴 ) ⊆ ( ◡ 𝐹 “ 𝐵 ) )