Theorem vextru

Description: Every setvar is a member of { x | T. } , which is therefore "a" universal class. Once class extensionality dfcleq is available, we can say "the" universal class (see df-v ). This is sbtru expressed using class abstractions. (Contributed by BJ, 2-Sep-2023)

	Ref	Expression
Assertion	vextru	⊢ 𝑦 ∈ { 𝑥 ∣ ⊤ }

Proof

Step	Hyp	Ref	Expression
1		tru	⊢ ⊤
2	1	vexw	⊢ 𝑦 ∈ { 𝑥 ∣ ⊤ }