Description: Equality theorem for function operation. (Contributed by Mario Carneiro, 20-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | ofeq | ⊢ ( 𝑅 = 𝑆 → ∘f 𝑅 = ∘f 𝑆 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | ⊢ ( 𝑅 = 𝑆 → 𝑅 = 𝑆 ) | |
2 | 1 | ofeqd | ⊢ ( 𝑅 = 𝑆 → ∘f 𝑅 = ∘f 𝑆 ) |