MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-subs Structured version   Visualization version   GIF version

Definition df-subs 27324
Description: Define surreal subtraction. (Contributed by Scott Fenton, 20-Aug-2024.)
Assertion
Ref Expression
df-subs -s = (𝑥 No , 𝑦 No ↦ (𝑥 +s ( -us𝑦)))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-subs
StepHypRef Expression
1 csubs 27322 . 2 class -s
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 csur 26991 . . 3 class No
52cv 1541 . . . 4 class 𝑥
63cv 1541 . . . . 5 class 𝑦
7 cnegs 27321 . . . . 5 class -us
86, 7cfv 6497 . . . 4 class ( -us𝑦)
9 cadds 27274 . . . 4 class +s
105, 8, 9co 7358 . . 3 class (𝑥 +s ( -us𝑦))
112, 3, 4, 4, 10cmpo 7360 . 2 class (𝑥 No , 𝑦 No ↦ (𝑥 +s ( -us𝑦)))
121, 11wceq 1542 1 wff -s = (𝑥 No , 𝑦 No ↦ (𝑥 +s ( -us𝑦)))
Colors of variables: wff setvar class
This definition is referenced by:  subsfn  27326  subsval  27354
  Copyright terms: Public domain W3C validator