Metamath Proof Explorer

Theorem elrnmpog

Description: Membership in the range of an operation class abstraction. (Contributed by NM, 27-Aug-2007) (Revised by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Hypothesis	rngop.1	$⊢ F = (x \in A, y \in B ⟼ C)$
	Assertion	elrnmpog	$⊢ D \in V \to (D \in ran F \leftrightarrow \exists x \in A \exists y \in B D = C)$

Step	Hyp	Ref	Expression
1		rngop.1	$⊢ F = (x \in A, y \in B ⟼ C)$
2		eqeq1	$⊢ z = D \to (z = C \leftrightarrow D = C)$
3	2	2rexbidv	$⊢ z = D \to (\exists x \in A \exists y \in B z = C \leftrightarrow \exists x \in A \exists y \in B D = C)$
4	1	rnmpo	$⊢ ran F = \{z \| \exists x \in A \exists y \in B z = C\}$
5	3 4	elab2g	$⊢ D \in V \to (D \in ran F \leftrightarrow \exists x \in A \exists y \in B D = C)$