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

Metamath Proof Explorer

Theorem ressid2

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

Ref Expression
Hypotheses ressbas.r ⊢ R = W ↾ 𝑠 A
ressbas.b ⊢ B = Base W
Assertion ressid2 ⊢ B ⊆ A ∧ W ∈ X ∧ A ∈ Y → R = W

Proof

Step Hyp Ref Expression
1 ressbas.r ⊢ R = W ↾ 𝑠 A
2 ressbas.b ⊢ B = Base W
3 1 2 ressval ⊢ W ∈ X ∧ A ∈ Y → R = if B ⊆ A W W sSet Base ndx A ∩ B
4 iftrue ⊢ B ⊆ A → if B ⊆ A W W sSet Base ndx A ∩ B = W
5 3 4 sylan9eqr ⊢ B ⊆ A ∧ W ∈ X ∧ A ∈ Y → R = W
6 5 3impb ⊢ B ⊆ A ∧ W ∈ X ∧ A ∈ Y → R = W