Metamath Proof Explorer


Theorem scottex2

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

Ref Expression
Assertion scottex2 Scott A V

Proof

Step Hyp Ref Expression
1 df-scott Scott A = x A | y A rank x rank y
2 scottex x A | y A rank x rank y V
3 1 2 eqeltri Scott A V