Metamath Proof Explorer

Theorem dfv2

Description: Alternate definition of the universal class (see df-v ). (Contributed by BJ, 30-Nov-2019)

Ref Expression
Assertion dfv2 
|- _V = { x | T. }

Proof

Step Hyp Ref Expression
1 df-v 
 |-  _V = { x | x = x }
2 equid 
 |-  x = x
3 2 bitru 
 |-  ( x = x <-> T. )
4 3 abbii 
 |-  { x | x = x } = { x | T. }
5 1 4 eqtri 
 |-  _V = { x | T. }