Definition df-v 2737

Description: Define the universal class. Definition 5.20 of [TakeutiZaring] p. 21. Also Definition 2.9 of [Quine] p. 19. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-v	|- _V = { x | x = x }

Detailed syntax breakdown of Definition df-v

Step	Hyp	Ref	Expression
1		cvv 2735	. 2 class _V
2		vx	. . . 4 setvar x
3	2, 2	weq 1501	. . 3 wff x = x
4	3, 2	cab 2161	. 2 class { x | x = x }
5	1, 4	wceq 1353	1 wff _V = { x | x = x }

This definition is referenced by:  vex  2738  int0  3854  ruv  4543  dcextest  4574  snexxph  6939