Theorem elabrexg

Description: Elementhood in an image set. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	elabrexg	$$⊢\left(x\in A\wedge B\in V\right)\to B\in \left\{y|\exists x\in Ay=B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		tru	$$⊢\top$$
2		csbeq1a	$$⊢x=z\to B=⦋z/x⦌B$$
3	2	equcoms	$$⊢z=x\to B=⦋z/x⦌B$$
4		trud	$$⊢z=x\to \top$$
5	3 4	2thd	$$⊢z=x\to \left(B=⦋z/x⦌B\leftrightarrow \top \right)$$
6	5	rspcev	$$⊢\left(x\in A\wedge \top \right)\to \exists z\in AB=⦋z/x⦌B$$
7	1 6	mpan2	$$⊢x\in A\to \exists z\in AB=⦋z/x⦌B$$
8	7	adantr	$$⊢\left(x\in A\wedge B\in V\right)\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	10	elabg	$$⊢B\in V\to \left(B\in \left\{y|\exists z\in Ay=⦋z/x⦌B\right\}\leftrightarrow \exists z\in AB=⦋z/x⦌B\right)$$
12	11	adantl	$$⊢\left(x\in A\wedge B\in V\right)\to \left(B\in \left\{y|\exists z\in Ay=⦋z/x⦌B\right\}\leftrightarrow \exists z\in AB=⦋z/x⦌B\right)$$
13	8 12	mpbird	$$⊢\left(x\in A\wedge B\in V\right)\to B\in \left\{y|\exists z\in Ay=⦋z/x⦌B\right\}$$
14		nfv	$$⊢Ⅎzy=B$$
15		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋z/x⦌B$$
16	15	nfeq2	$$⊢Ⅎxy=⦋z/x⦌B$$
17	2	eqeq2d	$$⊢x=z\to \left(y=B\leftrightarrow y=⦋z/x⦌B\right)$$
18	14 16 17	cbvrexw	$$⊢\exists x\in Ay=B\leftrightarrow \exists z\in Ay=⦋z/x⦌B$$
19	18	abbii	$$⊢\left\{y|\exists x\in Ay=B\right\}=\left\{y|\exists z\in Ay=⦋z/x⦌B\right\}$$
20	13 19	eleqtrrdi	$$⊢\left(x\in A\wedge B\in V\right)\to B\in \left\{y|\exists x\in Ay=B\right\}$$