# Metamath Proof Explorer

## Theorem colleq12d

Description: Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023)

Ref Expression
Hypotheses colleq12d.1 ${⊢}{\phi }\to {F}={G}$
colleq12d.2 ${⊢}{\phi }\to {A}={B}$
Assertion colleq12d ${⊢}{\phi }\to \left({F}Coll{A}\right)=\left({G}Coll{B}\right)$

### Proof

Step Hyp Ref Expression
1 colleq12d.1 ${⊢}{\phi }\to {F}={G}$
2 colleq12d.2 ${⊢}{\phi }\to {A}={B}$
3 1 imaeq1d ${⊢}{\phi }\to {F}\left[\left\{{x}\right\}\right]={G}\left[\left\{{x}\right\}\right]$
4 3 scotteqd ${⊢}{\phi }\to Scott{F}\left[\left\{{x}\right\}\right]=Scott{G}\left[\left\{{x}\right\}\right]$
5 2 4 iuneq12d ${⊢}{\phi }\to \bigcup _{{x}\in {A}}Scott{F}\left[\left\{{x}\right\}\right]=\bigcup _{{x}\in {B}}Scott{G}\left[\left\{{x}\right\}\right]$
6 df-coll ${⊢}\left({F}Coll{A}\right)=\bigcup _{{x}\in {A}}Scott{F}\left[\left\{{x}\right\}\right]$
7 df-coll ${⊢}\left({G}Coll{B}\right)=\bigcup _{{x}\in {B}}Scott{G}\left[\left\{{x}\right\}\right]$
8 5 6 7 3eqtr4g ${⊢}{\phi }\to \left({F}Coll{A}\right)=\left({G}Coll{B}\right)$