Metamath Proof Explorer


Theorem cleq1

Description: Equality of relations implies equality of closures. (Contributed by RP, 9-May-2020)

Ref Expression
Assertion cleq1
|- ( R = S -> |^| { r | ( R C_ r /\ ph ) } = |^| { r | ( S C_ r /\ ph ) } )

Proof

Step Hyp Ref Expression
1 cleq1lem
 |-  ( R = S -> ( ( R C_ r /\ ph ) <-> ( S C_ r /\ ph ) ) )
2 1 abbidv
 |-  ( R = S -> { r | ( R C_ r /\ ph ) } = { r | ( S C_ r /\ ph ) } )
3 2 inteqd
 |-  ( R = S -> |^| { r | ( R C_ r /\ ph ) } = |^| { r | ( S C_ r /\ ph ) } )