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

Metamath Proof Explorer

Theorem ressplusg

Description: +g is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014)

Ref Expression
Hypotheses ressplusg.1 ⊢ H = G ↾ 𝑠 A
ressplusg.2 ⊢ + ˙ = + G
Assertion ressplusg ⊢ A ∈ V → + ˙ = + H

Proof

Step Hyp Ref Expression
1 ressplusg.1 ⊢ H = G ↾ 𝑠 A
2 ressplusg.2 ⊢ + ˙ = + G
3 plusgid ⊢ + 𝑔 = Slot + ndx
4 basendxnplusgndx ⊢ Base ndx ≠ + ndx
5 4 necomi ⊢ + ndx ≠ Base ndx
6 1 2 3 5 resseqnbas ⊢ A ∈ V → + ˙ = + H