Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sgns Unicode version

Definition df-sgns 26650
Description: Signum function for a structure. See also df-sgn 12734 for the version for extended reals. (Contributed by Thierry Arnoux, 10-Sep-2018.)
Assertion
Ref Expression
df-sgns
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-sgns
StepHypRef Expression
1 csgns 26649 . 2
2 vr . . 3
3 cvv 3081 . . 3
4 vx . . . 4
52cv 1369 . . . . 5
6 cbs 14332 . . . . 5
75, 6cfv 5537 . . . 4
84cv 1369 . . . . . 6
9 c0g 14537 . . . . . . 7
105, 9cfv 5537 . . . . . 6
118, 10wceq 1370 . . . . 5
12 cc0 9419 . . . . 5
13 cplt 15270 . . . . . . . 8
145, 13cfv 5537 . . . . . . 7
1510, 8, 14wbr 4409 . . . . . 6
16 c1 9420 . . . . . 6
1716cneg 9733 . . . . . 6
1815, 16, 17cif 3905 . . . . 5
1911, 12, 18cif 3905 . . . 4
204, 7, 19cmpt 4467 . . 3
212, 3, 20cmpt 4467 . 2
221, 21wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  sgnsv  26651
  Copyright terms: Public domain W3C validator