Description: scottex expressed using Scott . (Contributed by Rohan Ridenour, 9-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | scottex2 | ⊢ Scott 𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-scott | ⊢ Scott 𝐴 = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } | |
2 | scottex | ⊢ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V | |
3 | 1 2 | eqeltri | ⊢ Scott 𝐴 ∈ V |