Metamath Proof Explorer


Theorem scottex2

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

Ref Expression
Assertion scottex2 Scott 𝐴 ∈ V

Proof

Step Hyp Ref Expression
1 df-scott Scott 𝐴 = { 𝑥𝐴 ∣ ∀ 𝑦𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) }
2 scottex { 𝑥𝐴 ∣ ∀ 𝑦𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V
3 1 2 eqeltri Scott 𝐴 ∈ V