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∈V
abrexco.2 ⊢y=B→C=D
Assertion abrexco ⊢x|∃y∈z|∃w∈Az=Bx=C=x|∃w∈Ax=D

Proof

Step Hyp Ref Expression
1 abrexco.1 ⊢B∈V
2 abrexco.2 ⊢y=B→C=D
3 df-rex ⊢∃y∈z|∃w∈Az=Bx=C↔∃yy∈z|∃w∈Az=B∧x=C
4 vex ⊢y∈V
5 eqeq1 ⊢z=y→z=B↔y=B
6 5 rexbidv ⊢z=y→∃w∈Az=B↔∃w∈Ay=B
7 4 6 elab ⊢y∈z|∃w∈Az=B↔∃w∈Ay=B
8 7 anbi1i ⊢y∈z|∃w∈Az=B∧x=C↔∃w∈Ay=B∧x=C
9 r19.41v ⊢∃w∈Ay=B∧x=C↔∃w∈Ay=B∧x=C
10 8 9 bitr4i ⊢y∈z|∃w∈Az=B∧x=C↔∃w∈Ay=B∧x=C
11 10 exbii ⊢∃yy∈z|∃w∈Az=B∧x=C↔∃y∃w∈Ay=B∧x=C
12 3 11 bitri ⊢∃y∈z|∃w∈Az=Bx=C↔∃y∃w∈Ay=B∧x=C
13 rexcom4 ⊢∃w∈A∃yy=B∧x=C↔∃y∃w∈Ay=B∧x=C
14 12 13 bitr4i ⊢∃y∈z|∃w∈Az=Bx=C↔∃w∈A∃yy=B∧x=C
15 2 eqeq2d ⊢y=B→x=C↔x=D
16 1 15 ceqsexv ⊢∃yy=B∧x=C↔x=D
17 16 rexbii ⊢∃w∈A∃yy=B∧x=C↔∃w∈Ax=D
18 14 17 bitri ⊢∃y∈z|∃w∈Az=Bx=C↔∃w∈Ax=D
19 18 abbii ⊢x|∃y∈z|∃w∈Az=Bx=C=x|∃w∈Ax=D