Metamath Proof Explorer

Theorem imaco

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

Ref Expression
Assertion imaco ⊢A∘BC=ABC

Proof

Step Hyp Ref Expression
1 df-rex ⊢∃y∈BCyAx↔∃yy∈BC∧yAx
2 vex ⊢x∈V
3 2 elima ⊢x∈ABC↔∃y∈BCyAx
4 rexcom4 ⊢∃z∈C∃yzBy∧yAx↔∃y∃z∈CzBy∧yAx
5 r19.41v ⊢∃z∈CzBy∧yAx↔∃z∈CzBy∧yAx
6 5 exbii ⊢∃y∃z∈CzBy∧yAx↔∃y∃z∈CzBy∧yAx
7 4 6 bitri ⊢∃z∈C∃yzBy∧yAx↔∃y∃z∈CzBy∧yAx
8 2 elima ⊢x∈A∘BC↔∃z∈CzA∘Bx
9 vex ⊢z∈V
10 9 2 brco ⊢zA∘Bx↔∃yzBy∧yAx
11 10 rexbii ⊢∃z∈CzA∘Bx↔∃z∈C∃yzBy∧yAx
12 8 11 bitri ⊢x∈A∘BC↔∃z∈C∃yzBy∧yAx
13 vex ⊢y∈V
14 13 elima ⊢y∈BC↔∃z∈CzBy
15 14 anbi1i ⊢y∈BC∧yAx↔∃z∈CzBy∧yAx
16 15 exbii ⊢∃yy∈BC∧yAx↔∃y∃z∈CzBy∧yAx
17 7 12 16 3bitr4i ⊢x∈A∘BC↔∃yy∈BC∧yAx
18 1 3 17 3bitr4ri ⊢x∈A∘BC↔x∈ABC
19 18 eqriv ⊢A∘BC=ABC