Description: Scott's trick produces a subset of the input class. (Contributed by Rohan Ridenour, 11-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | scottss | |- Scott A C_ A |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-scott | |- Scott A = { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } |
|
2 | 1 | ssrab3 | |- Scott A C_ A |