Definition df-l

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

	Ref	Expression
Assertion	df-l	Could not format assertion : No typesetting found for |- _L = ( _FL " On ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cl	Could not format _L : No typesetting found for class _L with typecode class
1		cfnl	Could not format _FL : No typesetting found for class _FL with typecode class
2		con0	$$class\mathrm{On}$$
3	1 2	cima	Could not format ( _FL " On ) : No typesetting found for class ( _FL " On ) with typecode class
4	0 3	wceq	Could not format _L = ( _FL " On ) : No typesetting found for wff _L = ( _FL " On ) with typecode wff