Definition df-l 35805

Description: Define the class of all constructible sets. Definition 15.15 of [TakeutiZaring] p. 158. (Contributed by BTernaryTau, 3-Sep-2026.)

Assertion

Ref	Expression
df-l	⊢ 𝐿 = (𝐹𝐿 “ On)

Detailed syntax breakdown of Definition df-l

Step	Hyp	Ref	Expression
1		cl 35796	. 2 class 𝐿
2		cfnl 35795	. . 3 class 𝐹𝐿
3		con0 6351	. . 3 class On
4	2, 3	cima 5650	. 2 class (𝐹𝐿 “ On)
5	1, 4	wceq 1570	1 wff 𝐿 = (𝐹𝐿 “ On)

This definition is used by: (None)