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

Metamath Proof Explorer

Theorem ressid

Description: Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014)

Ref Expression
Hypothesis ressid.1 ⊢ B = Base W
Assertion ressid ⊢ W ∈ X → W ↾ 𝑠 B = W

Proof

Step Hyp Ref Expression
1 ressid.1 ⊢ B = Base W
2 ssid ⊢ B ⊆ B
3 1 fvexi ⊢ B ∈ V
4 eqid ⊢ W ↾ 𝑠 B = W ↾ 𝑠 B
5 4 1 ressid2 ⊢ B ⊆ B ∧ W ∈ X ∧ B ∈ V → W ↾ 𝑠 B = W
6 2 3 5 mp3an13 ⊢ W ∈ X → W ↾ 𝑠 B = W