| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > fvoveq1 | Structured version Visualization version GIF version | ||
| Description: Equality theorem for nested function and operation value. Closed form of fvoveq1d 7453. (Contributed by AV, 23-Jul-2022.) |
| Ref | Expression |
|---|---|
| fvoveq1 | ⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id 22 | . 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) | |
| 2 | 1 | fvoveq1d 7453 | 1 ⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶))) |
| Copyright terms: Public domain | W3C validator |