Metamath Proof Explorer


Theorem pfxval

Description: Value of a prefix operation. (Contributed by AV, 2-May-2020)

Ref Expression
Assertion pfxval SVL0SprefixL=Ssubstr0L

Proof

Step Hyp Ref Expression
1 df-pfx prefix=sV,l0ssubstr0l
2 1 a1i SVL0prefix=sV,l0ssubstr0l
3 simpl s=Sl=Ls=S
4 opeq2 l=L0l=0L
5 4 adantl s=Sl=L0l=0L
6 3 5 oveq12d s=Sl=Lssubstr0l=Ssubstr0L
7 6 adantl SVL0s=Sl=Lssubstr0l=Ssubstr0L
8 elex SVSV
9 8 adantr SVL0SV
10 simpr SVL0L0
11 ovexd SVL0Ssubstr0LV
12 2 7 9 10 11 ovmpod SVL0SprefixL=Ssubstr0L