Metamath Proof Explorer

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 
|- _L = ( _FL " On )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cl 
 |-  _L
1 cfnl 
 |-  _FL
2 con0 
 |-  On
3 1 2 cima 
 |-  ( _FL " On )
4 0 3 wceq 
 |-  _L = ( _FL " On )