Definition df-v 1808

Description: Define the universal class. Definition 5.20 of [TakeutiZaring] p. 21.

Assertion

Ref	Expression
df-v	⊢ V = {x∣x = x}

Detailed syntax breakdown of Definition df-v

Step	Hyp	Ref	Expression
1		cvv 1807	. 2 class V
2		vx	. . . . 5 set x
3	2	cv 953	. . . 4 class x
4	3, 3	wceq 954	. . 3 wff x = x
5	4, 2	cab 1461	. 2 class {x∣x = x}
6	1, 5	wceq 954	1 wff V = {x∣x = x}

This definition is referenced by:  visset 1809  int0 2543  dmi 3326  fo1st 4092  fo2nd 4093

Copyright terms: Public domain