Metamath Proof Explorer

Theorem scottex2

Description: scottex expressed using Scott . (Contributed by Rohan Ridenour, 9-Aug-2023)

Ref Expression
Assertion scottex2 
|- Scott A e. _V

Proof

Step Hyp Ref Expression
1 df-scott 
 |-  Scott A = { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) }
2 scottex 
 |-  { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V
3 1 2 eqeltri 
 |-  Scott A e. _V