Description: Value of the Scott operation at a class abstraction. Variant of scottab using explicit substitution. (Contributed by Rohan Ridenour, 14-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | scottabes | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfs1v | |
|
2 | sbequ12 | |
|
3 | 1 2 | scottabf | |