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	|- Scott { x | ph } = { x | ( ph /\ A. y ( [ y / x ] ph -> ( rank ` x ) C_ ( rank ` y ) ) ) }

Proof

Step	Hyp	Ref	Expression
1		nfs1v	|- F/ x [ y / x ] ph
2		sbequ12	|- ( x = y -> ( ph <-> [ y / x ] ph ) )
3	1 2	scottabf	|- Scott { x | ph } = { x | ( ph /\ A. y ( [ y / x ] ph -> ( rank ` x ) C_ ( rank ` y ) ) ) }