This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ressstarv

Description: *r is unaffected by restriction. (Contributed by Mario Carneiro, 9-Oct-2015)

Ref Expression
Hypotheses ressmulr.1 ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
ressstarv.2 ⊢ ∗ = ( *𝑟 ‘ 𝑅 )
Assertion ressstarv ( 𝐴 ∈ 𝑉 → ∗ = ( *𝑟 ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 ressmulr.1 ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2 ressstarv.2 ⊢ ∗ = ( *𝑟 ‘ 𝑅 )
3 starvid ⊢ *𝑟 = Slot ( *𝑟 ‘ ndx )
4 starvndxnbasendx ⊢ ( *𝑟 ‘ ndx ) ≠ ( Base ‘ ndx )
5 1 2 3 4 resseqnbas ⊢ ( 𝐴 ∈ 𝑉 → ∗ = ( *𝑟 ‘ 𝑆 ) )