Theorem funimassov

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013)

	Ref	Expression
Assertion	funimassov	⊢ ( ( Fun 𝐹 ∧ ( 𝐴 × 𝐵 ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( 𝐴 × 𝐵 ) ) ⊆ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		funimass4	⊢ ( ( Fun 𝐹 ∧ ( 𝐴 × 𝐵 ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( 𝐴 × 𝐵 ) ) ⊆ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝐴 × 𝐵 ) ( 𝐹 ‘ 𝑧 ) ∈ 𝐶 ) )
2		fveq2	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
3		df-ov	⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
4	2 3	eqtr4di	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ 𝑧 ) = ( 𝑥 𝐹 𝑦 ) )
5	4	eleq1d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝐶 ↔ ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 ) )
6	5	ralxp	⊢ ( ∀ 𝑧 ∈ ( 𝐴 × 𝐵 ) ( 𝐹 ‘ 𝑧 ) ∈ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 )
7	1 6	bitrdi	⊢ ( ( Fun 𝐹 ∧ ( 𝐴 × 𝐵 ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( 𝐴 × 𝐵 ) ) ⊆ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 ) )