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

Metamath Proof Explorer

Theorem ressvsca

Description: .s is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Hypotheses resssca.1 ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
ressvsca.2 ⊢ · = ( ·𝑠 ‘ 𝐺 )
Assertion ressvsca ( 𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 resssca.1 ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
2 ressvsca.2 ⊢ · = ( ·𝑠 ‘ 𝐺 )
3 vscaid ⊢ ·𝑠 = Slot ( ·𝑠 ‘ ndx )
4 vscandxnbasendx ⊢ ( ·𝑠 ‘ ndx ) ≠ ( Base ‘ ndx )
5 1 2 3 4 resseqnbas ⊢ ( 𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘ 𝐻 ) )