Theorem elabrex

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

	Ref	Expression
Hypothesis	elabrex.1	|- B e. _V
Assertion	elabrex	|- ( x e. A -> B e. { y | E. x e. A y = B } )

Proof

Step	Hyp	Ref	Expression
1		elabrex.1	|- B e. _V
2		tru	|- T.
3		csbeq1a	|- ( x = z -> B = [_ z / x ]_ B )
4	3	equcoms	|- ( z = x -> B = [_ z / x ]_ B )
5		trud	|- ( z = x -> T. )
6	4 5	2thd	|- ( z = x -> ( B = [_ z / x ]_ B <-> T. ) )
7	6	rspcev	|- ( ( x e. A /\ T. ) -> E. z e. A B = [_ z / x ]_ B )
8	2 7	mpan2	|- ( x e. A -> E. z e. A B = [_ z / x ]_ B )
9		eqeq1	|- ( y = B -> ( y = [_ z / x ]_ B <-> B = [_ z / x ]_ B ) )
10	9	rexbidv	|- ( y = B -> ( E. z e. A y = [_ z / x ]_ B <-> E. z e. A B = [_ z / x ]_ B ) )
11	1 10	elab	|- ( B e. { y | E. z e. A y = [_ z / x ]_ B } <-> E. z e. A B = [_ z / x ]_ B )
12	8 11	sylibr	|- ( x e. A -> B e. { y | E. z e. A y = [_ z / x ]_ B } )
13		nfv	|- F/ z y = B
14		nfcsb1v	|- F/_ x [_ z / x ]_ B
15	14	nfeq2	|- F/ x y = [_ z / x ]_ B
16	3	eqeq2d	|- ( x = z -> ( y = B <-> y = [_ z / x ]_ B ) )
17	13 15 16	cbvrexw	|- ( E. x e. A y = B <-> E. z e. A y = [_ z / x ]_ B )
18	17	abbii	|- { y | E. x e. A y = B } = { y | E. z e. A y = [_ z / x ]_ B }
19	12 18	eleqtrrdi	|- ( x e. A -> B e. { y | E. x e. A y = B } )