Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  resvlem Structured version   Visualization version   Unicode version

Theorem resvlem 28594
 Description: Other elements of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
Hypotheses
Ref Expression
resvlem.r v
resvlem.e
resvlem.f Slot
resvlem.n
resvlem.b
Assertion
Ref Expression
resvlem

Proof of Theorem resvlem
StepHypRef Expression
1 resvlem.r . . . . . . 7 v
2 eqid 2451 . . . . . . 7 Scalar Scalar
3 eqid 2451 . . . . . . 7 Scalar Scalar
41, 2, 3resvid2 28591 . . . . . 6 Scalar
54fveq2d 5869 . . . . 5 Scalar
653expib 1211 . . . 4 Scalar
71, 2, 3resvval2 28592 . . . . . . 7 Scalar sSet Scalar Scalars
87fveq2d 5869 . . . . . 6 Scalar sSet Scalar Scalars
9 resvlem.f . . . . . . . 8 Slot
10 resvlem.n . . . . . . . 8
119, 10ndxid 15142 . . . . . . 7 Slot
129, 10ndxarg 15141 . . . . . . . . 9
13 resvlem.b . . . . . . . . 9
1412, 13eqnetri 2694 . . . . . . . 8
15 scandx 15257 . . . . . . . 8 Scalar
1614, 15neeqtrri 2697 . . . . . . 7 Scalar
1711, 16setsnid 15165 . . . . . 6 sSet Scalar Scalars
188, 17syl6eqr 2503 . . . . 5 Scalar
19183expib 1211 . . . 4 Scalar
206, 19pm2.61i 168 . . 3
21 reldmresv 28589 . . . . . . . . 9 v
2221ovprc1 6321 . . . . . . . 8 v
231, 22syl5eq 2497 . . . . . . 7
2423fveq2d 5869 . . . . . 6
259str0 15161 . . . . . 6
2624, 25syl6eqr 2503 . . . . 5
27 fvprc 5859 . . . . 5
2826, 27eqtr4d 2488 . . . 4