Definition df-v 2732

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 = {𝑥 ∣ 𝑥 = 𝑥}

Detailed syntax breakdown of Definition df-v

Step	Hyp	Ref	Expression
1		cvv 2730	. 2 class V
2		vx	. . . 4 setvar 𝑥
3	2, 2	weq 1496	. . 3 wff 𝑥 = 𝑥
4	3, 2	cab 2156	. 2 class {𝑥 ∣ 𝑥 = 𝑥}
5	1, 4	wceq 1348	1 wff V = {𝑥 ∣ 𝑥 = 𝑥}

This definition is referenced by:  vex  2733  int0  3845  ruv  4534  dcextest  4565  snexxph  6927