This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elimag

Description: Membership in an image. Theorem 34 of Suppes p. 65. (Contributed by NM, 20-Jan-2007)

		Ref	Expression
	Assertion	elimag	$⊢ A \in V \to (A \in B [C] \leftrightarrow \exists x \in C x B A)$

Step	Hyp	Ref	Expression
1		breq2	$⊢ y = A \to (x B y \leftrightarrow x B A)$
2	1	rexbidv	$⊢ y = A \to (\exists x \in C x B y \leftrightarrow \exists x \in C x B A)$
3		dfima2	$⊢ B [C] = \{y \| \exists x \in C x B y\}$
4	2 3	elab2g	$⊢ A \in V \to (A \in B [C] \leftrightarrow \exists x \in C x B A)$