This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ y ∈ x | ⊤

Proof

Step Hyp Ref Expression
1 tru ⊢ ⊤
2 1 vexw ⊢ y ∈ x | ⊤