Detailed syntax breakdown of Definition df-abss
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cabss 28261 | . 2
class
abss | 
| 2 |  | vx | . . 3
setvar 𝑥 | 
| 3 |  | csur 27684 | . . 3
class  No | 
| 4 |  | c0s 27867 | . . . . 5
class 
0s | 
| 5 | 2 | cv 1539 | . . . . 5
class 𝑥 | 
| 6 |  | csle 27789 | . . . . 5
class 
≤s | 
| 7 | 4, 5, 6 | wbr 5143 | . . . 4
wff 
0s ≤s 𝑥 | 
| 8 |  | cnegs 28051 | . . . . 5
class 
-us | 
| 9 | 5, 8 | cfv 6561 | . . . 4
class (
-us ‘𝑥) | 
| 10 | 7, 5, 9 | cif 4525 | . . 3
class if(
0s ≤s 𝑥,
𝑥, ( -us
‘𝑥)) | 
| 11 | 2, 3, 10 | cmpt 5225 | . 2
class (𝑥 ∈ 
No  ↦ if( 0s ≤s 𝑥, 𝑥, ( -us ‘𝑥))) | 
| 12 | 1, 11 | wceq 1540 | 1
wff
abss = (𝑥
∈  No  ↦ if( 0s ≤s 𝑥, 𝑥, ( -us ‘𝑥))) |