Metamath Proof Explorer


Theorem scotteq

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

Ref Expression
Assertion scotteq
|- ( A = B -> Scott A = Scott B )

Proof

Step Hyp Ref Expression
1 id
 |-  ( A = B -> A = B )
2 1 scotteqd
 |-  ( A = B -> Scott A = Scott B )