This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 }