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	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
	strssd.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
	strssd.f	⊢ ( 𝜑 → Fun 𝑇 )
	strssd.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝑇 )
	strssd.n	⊢ ( 𝜑 → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ 𝑆 )
Assertion	strssd	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑇 ) = ( 𝐸 ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		strssd.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
2		strssd.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
3		strssd.f	⊢ ( 𝜑 → Fun 𝑇 )
4		strssd.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝑇 )
5		strssd.n	⊢ ( 𝜑 → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ 𝑆 )
6	4 5	sseldd	⊢ ( 𝜑 → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ 𝑇 )
7	1 2 3 6	strfvd	⊢ ( 𝜑 → 𝐶 = ( 𝐸 ‘ 𝑇 ) )
8	2 4	ssexd	⊢ ( 𝜑 → 𝑆 ∈ V )
9		funss	⊢ ( 𝑆 ⊆ 𝑇 → ( Fun 𝑇 → Fun 𝑆 ) )
10	4 3 9	sylc	⊢ ( 𝜑 → Fun 𝑆 )
11	1 8 10 5	strfvd	⊢ ( 𝜑 → 𝐶 = ( 𝐸 ‘ 𝑆 ) )
12	7 11	eqtr3d	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑇 ) = ( 𝐸 ‘ 𝑆 ) )