fnrnov

Description: The range of an operation expressed as a collection of the operation's values. (Contributed by NM, 29-Oct-2006)

		Ref	Expression
	Assertion	fnrnov	$⊢ F Fn (A \times B) \to ran F = \{z \| \exists x \in A \exists y \in B z = x F y\}$

Step	Hyp	Ref	Expression
1		fnrnfv	$⊢ F Fn (A \times B) \to ran F = \{z \| \exists w \in (A \times B) z = F (w)\}$
2		fveq2	$⊢ w = ⟨x, y⟩ \to F (w) = F (⟨x, y⟩)$
3		df-ov	$⊢ x F y = F (⟨x, y⟩)$
4	2 3	eqtr4di	$⊢ w = ⟨x, y⟩ \to F (w) = x F y$
5	4	eqeq2d	$⊢ w = ⟨x, y⟩ \to (z = F (w) \leftrightarrow z = x F y)$
6	5	rexxp	$⊢ \exists w \in (A \times B) z = F (w) \leftrightarrow \exists x \in A \exists y \in B z = x F y$
7	6	abbii	$⊢ \{z \| \exists w \in (A \times B) z = F (w)\} = \{z \| \exists x \in A \exists y \in B z = x F y\}$
8	1 7	eqtrdi	$⊢ F Fn (A \times B) \to ran F = \{z \| \exists x \in A \exists y \in B z = x F y\}$

Metamath Proof Explorer