# Metamath Proof Explorer

## Theorem imaco

Description: Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006)

Ref Expression
Assertion imaco ${⊢}\left({A}\circ {B}\right)\left[{C}\right]={A}\left[{B}\left[{C}\right]\right]$

### Proof

Step Hyp Ref Expression
1 df-rex ${⊢}\exists {y}\in {B}\left[{C}\right]\phantom{\rule{.4em}{0ex}}{y}{A}{x}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\left[{C}\right]\wedge {y}{A}{x}\right)$
2 vex ${⊢}{x}\in \mathrm{V}$
3 2 elima ${⊢}{x}\in {A}\left[{B}\left[{C}\right]\right]↔\exists {y}\in {B}\left[{C}\right]\phantom{\rule{.4em}{0ex}}{y}{A}{x}$
4 rexcom4 ${⊢}\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}{B}{y}\wedge {y}{A}{x}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}\left({z}{B}{y}\wedge {y}{A}{x}\right)$
5 r19.41v ${⊢}\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}\left({z}{B}{y}\wedge {y}{A}{x}\right)↔\left(\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{z}{B}{y}\wedge {y}{A}{x}\right)$
6 5 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}\left({z}{B}{y}\wedge {y}{A}{x}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{z}{B}{y}\wedge {y}{A}{x}\right)$
7 4 6 bitri ${⊢}\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}{B}{y}\wedge {y}{A}{x}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{z}{B}{y}\wedge {y}{A}{x}\right)$
8 2 elima ${⊢}{x}\in \left({A}\circ {B}\right)\left[{C}\right]↔\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{z}\left({A}\circ {B}\right){x}$
9 vex ${⊢}{z}\in \mathrm{V}$
10 9 2 brco ${⊢}{z}\left({A}\circ {B}\right){x}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}{B}{y}\wedge {y}{A}{x}\right)$
11 10 rexbii ${⊢}\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{z}\left({A}\circ {B}\right){x}↔\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}{B}{y}\wedge {y}{A}{x}\right)$
12 8 11 bitri ${⊢}{x}\in \left({A}\circ {B}\right)\left[{C}\right]↔\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}{B}{y}\wedge {y}{A}{x}\right)$
13 vex ${⊢}{y}\in \mathrm{V}$
14 13 elima ${⊢}{y}\in {B}\left[{C}\right]↔\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{z}{B}{y}$
15 14 anbi1i ${⊢}\left({y}\in {B}\left[{C}\right]\wedge {y}{A}{x}\right)↔\left(\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{z}{B}{y}\wedge {y}{A}{x}\right)$
16 15 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\left[{C}\right]\wedge {y}{A}{x}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\in {C}\phantom{\rule{.4em}{0ex}}{z}{B}{y}\wedge {y}{A}{x}\right)$
17 7 12 16 3bitr4i ${⊢}{x}\in \left({A}\circ {B}\right)\left[{C}\right]↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\left[{C}\right]\wedge {y}{A}{x}\right)$
18 1 3 17 3bitr4ri ${⊢}{x}\in \left({A}\circ {B}\right)\left[{C}\right]↔{x}\in {A}\left[{B}\left[{C}\right]\right]$
19 18 eqriv ${⊢}\left({A}\circ {B}\right)\left[{C}\right]={A}\left[{B}\left[{C}\right]\right]$