Metamath Proof Explorer

Theorem ovelrn

Description: A member of an operation's range is a value of the operation. (Contributed by NM, 7-Feb-2007) (Revised by Mario Carneiro, 30-Jan-2014)

		Ref	Expression
	Assertion	ovelrn	$⊢ F Fn (A \times B) \to (C \in ran F \leftrightarrow \exists x \in A \exists y \in B C = x F y)$

Proof

Step	Hyp	Ref	Expression
1		fnrnov	$⊢ F Fn (A \times B) \to ran F = \{z \| \exists x \in A \exists y \in B z = x F y\}$
2	1	eleq2d	$⊢ F Fn (A \times B) \to (C \in ran F \leftrightarrow C \in \{z \| \exists x \in A \exists y \in B z = x F y\})$
3		ovex	$⊢ x F y \in V$
4		eleq1	$⊢ C = x F y \to (C \in V \leftrightarrow x F y \in V)$
5	3 4	mpbiri	$⊢ C = x F y \to C \in V$
6	5	rexlimivw	$⊢ \exists y \in B C = x F y \to C \in V$
7	6	rexlimivw	$⊢ \exists x \in A \exists y \in B C = x F y \to C \in V$
8		eqeq1	$⊢ z = C \to (z = x F y \leftrightarrow C = x F y)$
9	8	2rexbidv	$⊢ z = C \to (\exists x \in A \exists y \in B z = x F y \leftrightarrow \exists x \in A \exists y \in B C = x F y)$
10	7 9	elab3	$⊢ C \in \{z \| \exists x \in A \exists y \in B z = x F y\} \leftrightarrow \exists x \in A \exists y \in B C = x F y$
11	2 10	bitrdi	$⊢ F Fn (A \times B) \to (C \in ran F \leftrightarrow \exists x \in A \exists y \in B C = x F y)$