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