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 \left(A\in B\left[C\right]\leftrightarrow \exists x\in CxBA\right)$$

Proof

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