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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru | |
|
2 | 1 | vexw | |