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