Theorem abrexco

Description: Composition of two image maps C ( y ) and B ( w ) . (Contributed by NM, 27-May-2013)

	Ref	Expression
Hypotheses	abrexco.1	|- B e. _V
	abrexco.2	|- ( y = B -> C = D )
Assertion	abrexco	|- { x | E. y e. { z | E. w e. A z = B } x = C } = { x | E. w e. A x = D }

Proof

Step	Hyp	Ref	Expression
1		abrexco.1	|- B e. _V
2		abrexco.2	|- ( y = B -> C = D )
3		df-rex	|- ( E. y e. { z | E. w e. A z = B } x = C <-> E. y ( y e. { z | E. w e. A z = B } /\ x = C ) )
4		vex	|- y e. _V
5		eqeq1	|- ( z = y -> ( z = B <-> y = B ) )
6	5	rexbidv	|- ( z = y -> ( E. w e. A z = B <-> E. w e. A y = B ) )
7	4 6	elab	|- ( y e. { z | E. w e. A z = B } <-> E. w e. A y = B )
8	7	anbi1i	|- ( ( y e. { z | E. w e. A z = B } /\ x = C ) <-> ( E. w e. A y = B /\ x = C ) )
9		r19.41v	|- ( E. w e. A ( y = B /\ x = C ) <-> ( E. w e. A y = B /\ x = C ) )
10	8 9	bitr4i	|- ( ( y e. { z | E. w e. A z = B } /\ x = C ) <-> E. w e. A ( y = B /\ x = C ) )
11	10	exbii	|- ( E. y ( y e. { z | E. w e. A z = B } /\ x = C ) <-> E. y E. w e. A ( y = B /\ x = C ) )
12	3 11	bitri	|- ( E. y e. { z | E. w e. A z = B } x = C <-> E. y E. w e. A ( y = B /\ x = C ) )
13		rexcom4	|- ( E. w e. A E. y ( y = B /\ x = C ) <-> E. y E. w e. A ( y = B /\ x = C ) )
14	12 13	bitr4i	|- ( E. y e. { z | E. w e. A z = B } x = C <-> E. w e. A E. y ( y = B /\ x = C ) )
15	2	eqeq2d	|- ( y = B -> ( x = C <-> x = D ) )
16	1 15	ceqsexv	|- ( E. y ( y = B /\ x = C ) <-> x = D )
17	16	rexbii	|- ( E. w e. A E. y ( y = B /\ x = C ) <-> E. w e. A x = D )
18	14 17	bitri	|- ( E. y e. { z | E. w e. A z = B } x = C <-> E. w e. A x = D )
19	18	abbii	|- { x | E. y e. { z | E. w e. A z = B } x = C } = { x | E. w e. A x = D }