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

Metamath Proof Explorer

Theorem strssd

Description: Deduction version of strss . (Contributed by Mario Carneiro, 15-Nov-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses strssd.e ⊢ E = Slot E ⁡ ndx
strssd.t ⊢ φ → T ∈ V
strssd.f ⊢ φ → Fun ⁡ T
strssd.s ⊢ φ → S ⊆ T
strssd.n ⊢ φ → E ⁡ ndx C ∈ S
Assertion strssd ⊢ φ → E ⁡ T = E ⁡ S

Proof

Step Hyp Ref Expression
1 strssd.e ⊢ E = Slot E ⁡ ndx
2 strssd.t ⊢ φ → T ∈ V
3 strssd.f ⊢ φ → Fun ⁡ T
4 strssd.s ⊢ φ → S ⊆ T
5 strssd.n ⊢ φ → E ⁡ ndx C ∈ S
6 4 5 sseldd ⊢ φ → E ⁡ ndx C ∈ T
7 1 2 3 6 strfvd ⊢ φ → C = E ⁡ T
8 2 4 ssexd ⊢ φ → S ∈ V
9 funss ⊢ S ⊆ T → Fun ⁡ T → Fun ⁡ S
10 4 3 9 sylc ⊢ φ → Fun ⁡ S
11 1 8 10 5 strfvd ⊢ φ → C = E ⁡ S
12 7 11 eqtr3d ⊢ φ → E ⁡ T = E ⁡ S