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 = R ↾ 𝑠 A
ressstarv.2 ⊢ ∗ ˙ = * R
Assertion ressstarv ⊢ A ∈ V → ∗ ˙ = * S

Proof

Step Hyp Ref Expression
1 ressmulr.1 ⊢ S = R ↾ 𝑠 A
2 ressstarv.2 ⊢ ∗ ˙ = * R
3 starvid ⊢ ∗ 𝑟 = Slot * ndx
4 starvndxnbasendx ⊢ * ndx ≠ Base ndx
5 1 2 3 4 resseqnbas ⊢ A ∈ V → ∗ ˙ = * S