Metamath Proof Explorer


Theorem scotteq

Description: Closed form of scotteqd . (Contributed by Rohan Ridenour, 9-Aug-2023)

Ref Expression
Assertion scotteq ( 𝐴 = 𝐵 → Scott 𝐴 = Scott 𝐵 )

Proof

Step Hyp Ref Expression
1 id ( 𝐴 = 𝐵𝐴 = 𝐵 )
2 1 scotteqd ( 𝐴 = 𝐵 → Scott 𝐴 = Scott 𝐵 )