Metamath Proof Explorer


Theorem scottabes

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 Scottx|φ=x|φyyxφrankxranky

Proof

Step Hyp Ref Expression
1 nfs1v xyxφ
2 sbequ12 x=yφyxφ
3 1 2 scottabf Scottx|φ=x|φyyxφrankxranky