# Metamath Proof Explorer

## Theorem imaco

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

Ref Expression
Assertion imaco ( ( 𝐴𝐵 ) “ 𝐶 ) = ( 𝐴 “ ( 𝐵𝐶 ) )

### Proof

Step Hyp Ref Expression
1 df-rex ( ∃ 𝑦 ∈ ( 𝐵𝐶 ) 𝑦 𝐴 𝑥 ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝐵𝐶 ) ∧ 𝑦 𝐴 𝑥 ) )
2 vex 𝑥 ∈ V
3 2 elima ( 𝑥 ∈ ( 𝐴 “ ( 𝐵𝐶 ) ) ↔ ∃ 𝑦 ∈ ( 𝐵𝐶 ) 𝑦 𝐴 𝑥 )
4 rexcom4 ( ∃ 𝑧𝐶𝑦 ( 𝑧 𝐵 𝑦𝑦 𝐴 𝑥 ) ↔ ∃ 𝑦𝑧𝐶 ( 𝑧 𝐵 𝑦𝑦 𝐴 𝑥 ) )
5 r19.41v ( ∃ 𝑧𝐶 ( 𝑧 𝐵 𝑦𝑦 𝐴 𝑥 ) ↔ ( ∃ 𝑧𝐶 𝑧 𝐵 𝑦𝑦 𝐴 𝑥 ) )
6 5 exbii ( ∃ 𝑦𝑧𝐶 ( 𝑧 𝐵 𝑦𝑦 𝐴 𝑥 ) ↔ ∃ 𝑦 ( ∃ 𝑧𝐶 𝑧 𝐵 𝑦𝑦 𝐴 𝑥 ) )
7 4 6 bitri ( ∃ 𝑧𝐶𝑦 ( 𝑧 𝐵 𝑦𝑦 𝐴 𝑥 ) ↔ ∃ 𝑦 ( ∃ 𝑧𝐶 𝑧 𝐵 𝑦𝑦 𝐴 𝑥 ) )
8 2 elima ( 𝑥 ∈ ( ( 𝐴𝐵 ) “ 𝐶 ) ↔ ∃ 𝑧𝐶 𝑧 ( 𝐴𝐵 ) 𝑥 )
9 vex 𝑧 ∈ V
10 9 2 brco ( 𝑧 ( 𝐴𝐵 ) 𝑥 ↔ ∃ 𝑦 ( 𝑧 𝐵 𝑦𝑦 𝐴 𝑥 ) )
11 10 rexbii ( ∃ 𝑧𝐶 𝑧 ( 𝐴𝐵 ) 𝑥 ↔ ∃ 𝑧𝐶𝑦 ( 𝑧 𝐵 𝑦𝑦 𝐴 𝑥 ) )
12 8 11 bitri ( 𝑥 ∈ ( ( 𝐴𝐵 ) “ 𝐶 ) ↔ ∃ 𝑧𝐶𝑦 ( 𝑧 𝐵 𝑦𝑦 𝐴 𝑥 ) )
13 vex 𝑦 ∈ V
14 13 elima ( 𝑦 ∈ ( 𝐵𝐶 ) ↔ ∃ 𝑧𝐶 𝑧 𝐵 𝑦 )
15 14 anbi1i ( ( 𝑦 ∈ ( 𝐵𝐶 ) ∧ 𝑦 𝐴 𝑥 ) ↔ ( ∃ 𝑧𝐶 𝑧 𝐵 𝑦𝑦 𝐴 𝑥 ) )
16 15 exbii ( ∃ 𝑦 ( 𝑦 ∈ ( 𝐵𝐶 ) ∧ 𝑦 𝐴 𝑥 ) ↔ ∃ 𝑦 ( ∃ 𝑧𝐶 𝑧 𝐵 𝑦𝑦 𝐴 𝑥 ) )
17 7 12 16 3bitr4i ( 𝑥 ∈ ( ( 𝐴𝐵 ) “ 𝐶 ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝐵𝐶 ) ∧ 𝑦 𝐴 𝑥 ) )
18 1 3 17 3bitr4ri ( 𝑥 ∈ ( ( 𝐴𝐵 ) “ 𝐶 ) ↔ 𝑥 ∈ ( 𝐴 “ ( 𝐵𝐶 ) ) )
19 18 eqriv ( ( 𝐴𝐵 ) “ 𝐶 ) = ( 𝐴 “ ( 𝐵𝐶 ) )