Metamath Proof Explorer

Theorem colleq2

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

Ref Expression
Assertion colleq2 
|- ( A = B -> ( F Coll A ) = ( F Coll B ) )

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( A = B -> F = F )
2 id 
 |-  ( A = B -> A = B )
3 1 2 colleq12d 
 |-  ( A = B -> ( F Coll A ) = ( F Coll B ) )