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 𝐵 ) )