Theorem scottab

Description: Value of the Scott operation at a class abstraction. (Contributed by Rohan Ridenour, 14-Aug-2023)

	Ref	Expression
Hypothesis	scottab.1	|- ( x = y -> ( ph <-> ps ) )
Assertion	scottab	|- Scott { x | ph } = { x | ( ph /\ A. y ( ps -> ( rank ` x ) C_ ( rank ` y ) ) ) }

Proof

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