Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rgspn Structured version   Unicode version

Definition df-rgspn 17942
 Description: The ring-span of a set of elements in a ring is the smallest subring which contains all of them. (Contributed by Stefan O'Rear, 7-Dec-2014.)
Assertion
Ref Expression
df-rgspn RingSpan SubRing
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-rgspn
StepHypRef Expression
1 crgspn 17940 . 2 RingSpan
2 vw . . 3
3 cvv 3087 . . 3
4 vs . . . 4
52cv 1436 . . . . . 6
6 cbs 15084 . . . . . 6
75, 6cfv 5601 . . . . 5
87cpw 3985 . . . 4
94cv 1436 . . . . . . 7
10 vt . . . . . . . 8
1110cv 1436 . . . . . . 7
129, 11wss 3442 . . . . . 6
13 csubrg 17939 . . . . . . 7 SubRing
145, 13cfv 5601 . . . . . 6 SubRing
1512, 10, 14crab 2786 . . . . 5 SubRing
1615cint 4258 . . . 4 SubRing
174, 8, 16cmpt 4484 . . 3 SubRing
182, 3, 17cmpt 4484 . 2 SubRing
191, 18wceq 1437 1 RingSpan SubRing
 Colors of variables: wff setvar class This definition is referenced by:  rgspnval  35733
 Copyright terms: Public domain W3C validator