Definition df-v 2294

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 2292	. 2 class _V
2		vx	. . . . 5 set x
3	2	cv 1297	. . . 4 class x
4	3, 3	wceq 1298	. . 3 wff x = x
5	4, 2	cab 1871	. 2 class {x | x = x}
6	1, 5	wceq 1298	1 wff _V = {x | x = x}

This definition is referenced by:  visset 2295  int0 3230  dmiOLD 4173  fo1st 5032  fo2nd 5033  ruv 5704  foo3 12015  domep 13861  elnev 16404

Copyright terms: Public domain