Theorem funimass5

Description: A subclass of a preimage in terms of function values. (Contributed by NM, 15-May-2007)

	Ref	Expression
Assertion	funimass5	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐴 ⊆ ( ◡ 𝐹 “ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		funimass3	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ 𝐴 ⊆ ( ◡ 𝐹 “ 𝐵 ) ) )
2		funimass4	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
3	1 2	bitr3d	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐴 ⊆ ( ◡ 𝐹 “ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )