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

Metamath Proof Explorer

Theorem ressds

Description: dist is unaffected by restriction. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypotheses ressds.1 ⊢ H = G ↾ 𝑠 A
ressds.2 ⊢ D = dist ⁡ G
Assertion ressds ⊢ A ∈ V → D = dist ⁡ H

Proof

Step Hyp Ref Expression
1 ressds.1 ⊢ H = G ↾ 𝑠 A
2 ressds.2 ⊢ D = dist ⁡ G
3 dsid ⊢ dist = Slot dist ⁡ ndx
4 dsndxnbasendx ⊢ dist ⁡ ndx ≠ Base ndx
5 1 2 3 4 resseqnbas ⊢ A ∈ V → D = dist ⁡ H