Description: Closed form of scotteqd . (Contributed by Rohan Ridenour, 9-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | scotteq | |- ( A = B -> Scott A = Scott B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | |- ( A = B -> A = B ) |
|
2 | 1 | scotteqd | |- ( A = B -> Scott A = Scott B ) |