Metamath Proof Explorer

Theorem scottex2OLD

Description: Obsolete version of scottex as of 18-Jul-2026. (Contributed by Rohan Ridenour, 9-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion scottex2OLD 
|- 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 scottexOLD 
 |-  { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V
3 1 2 eqeltri 
 |-  Scott A e. _V