Theorem elabrex

Description: Elementhood in an image set. (Contributed by Mario Carneiro, 14-Jan-2014)

	Ref	Expression
Hypothesis	elabrex.1	$$⊢B\in \mathrm{V}$$
Assertion	elabrex	$$⊢x\in A\to B\in \left\{y|\exists x\in Ay=B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		elabrex.1	$$⊢B\in \mathrm{V}$$
2		tru	$$⊢\top$$
3		csbeq1a	$$⊢x=z\to B=⦋z/x⦌B$$
4	3	equcoms	$$⊢z=x\to B=⦋z/x⦌B$$
5		trud	$$⊢z=x\to \top$$
6	4 5	2thd	$$⊢z=x\to \left(B=⦋z/x⦌B\leftrightarrow \top \right)$$
7	6	rspcev	$$⊢\left(x\in A\wedge \top \right)\to \exists z\in AB=⦋z/x⦌B$$
8	2 7	mpan2	$$⊢x\in A\to \exists z\in AB=⦋z/x⦌B$$
9		eqeq1	$$⊢y=B\to \left(y=⦋z/x⦌B\leftrightarrow B=⦋z/x⦌B\right)$$
10	9	rexbidv	$$⊢y=B\to \left(\exists z\in Ay=⦋z/x⦌B\leftrightarrow \exists z\in AB=⦋z/x⦌B\right)$$
11	1 10	elab	$$⊢B\in \left\{y|\exists z\in Ay=⦋z/x⦌B\right\}\leftrightarrow \exists z\in AB=⦋z/x⦌B$$
12	8 11	sylibr	$$⊢x\in A\to B\in \left\{y|\exists z\in Ay=⦋z/x⦌B\right\}$$
13		nfv	$$⊢Ⅎzy=B$$
14		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋z/x⦌B$$
15	14	nfeq2	$$⊢Ⅎxy=⦋z/x⦌B$$
16	3	eqeq2d	$$⊢x=z\to \left(y=B\leftrightarrow y=⦋z/x⦌B\right)$$
17	13 15 16	cbvrexw	$$⊢\exists x\in Ay=B\leftrightarrow \exists z\in Ay=⦋z/x⦌B$$
18	17	abbii	$$⊢\left\{y|\exists x\in Ay=B\right\}=\left\{y|\exists z\in Ay=⦋z/x⦌B\right\}$$
19	12 18	eleqtrrdi	$$⊢x\in A\to B\in \left\{y|\exists x\in Ay=B\right\}$$