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 F \land A \times B \subseteq dom F) \to (F [A \times B] \subseteq C \leftrightarrow \forall x \in A \forall y \in B x F y \in C)$

Step	Hyp	Ref	Expression
1		funimass4	$⊢ (Fun F \land A \times B \subseteq dom F) \to (F [A \times B] \subseteq C \leftrightarrow \forall z \in (A \times B) F (z) \in C)$
2		fveq2	$⊢ z = ⟨x, y⟩ \to F (z) = F (⟨x, y⟩)$
3		df-ov	$⊢ x F y = F (⟨x, y⟩)$
4	2 3	eqtr4di	$⊢ z = ⟨x, y⟩ \to F (z) = x F y$
5	4	eleq1d	$⊢ z = ⟨x, y⟩ \to (F (z) \in C \leftrightarrow x F y \in C)$
6	5	ralxp	$⊢ \forall z \in (A \times B) F (z) \in C \leftrightarrow \forall x \in A \forall y \in B x F y \in C$
7	1 6	bitrdi	$⊢ (Fun F \land A \times B \subseteq dom F) \to (F [A \times B] \subseteq C \leftrightarrow \forall x \in A \forall y \in B x F y \in C)$

Metamath Proof Explorer