Metamath Proof Explorer


Theorem colleq12d

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

Ref Expression
Hypotheses colleq12d.1 ( 𝜑𝐹 = 𝐺 )
colleq12d.2 ( 𝜑𝐴 = 𝐵 )
Assertion colleq12d ( 𝜑 → ( 𝐹 Coll 𝐴 ) = ( 𝐺 Coll 𝐵 ) )

Proof

Step Hyp Ref Expression
1 colleq12d.1 ( 𝜑𝐹 = 𝐺 )
2 colleq12d.2 ( 𝜑𝐴 = 𝐵 )
3 1 imaeq1d ( 𝜑 → ( 𝐹 “ { 𝑥 } ) = ( 𝐺 “ { 𝑥 } ) )
4 3 scotteqd ( 𝜑 → Scott ( 𝐹 “ { 𝑥 } ) = Scott ( 𝐺 “ { 𝑥 } ) )
5 2 4 iuneq12d ( 𝜑 𝑥𝐴 Scott ( 𝐹 “ { 𝑥 } ) = 𝑥𝐵 Scott ( 𝐺 “ { 𝑥 } ) )
6 df-coll ( 𝐹 Coll 𝐴 ) = 𝑥𝐴 Scott ( 𝐹 “ { 𝑥 } )
7 df-coll ( 𝐺 Coll 𝐵 ) = 𝑥𝐵 Scott ( 𝐺 “ { 𝑥 } )
8 5 6 7 3eqtr4g ( 𝜑 → ( 𝐹 Coll 𝐴 ) = ( 𝐺 Coll 𝐵 ) )