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 𝐴 ∈ V

Proof

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