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=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
	strssd.t	$$⊢\phi \to T\in V$$
	strssd.f	$$⊢\phi \to \mathrm{Fun}T$$
	strssd.s	$$⊢\phi \to S\subseteq T$$
	strssd.n	$$⊢\phi \to ⟨E\left(\mathrm{ndx}\right),C⟩\in S$$
Assertion	strssd	$$⊢\phi \to E\left(T\right)=E\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		strssd.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
2		strssd.t	$$⊢\phi \to T\in V$$
3		strssd.f	$$⊢\phi \to \mathrm{Fun}T$$
4		strssd.s	$$⊢\phi \to S\subseteq T$$
5		strssd.n	$$⊢\phi \to ⟨E\left(\mathrm{ndx}\right),C⟩\in S$$
6	4 5	sseldd	$$⊢\phi \to ⟨E\left(\mathrm{ndx}\right),C⟩\in T$$
7	1 2 3 6	strfvd	$$⊢\phi \to C=E\left(T\right)$$
8	2 4	ssexd	$$⊢\phi \to S\in \mathrm{V}$$
9		funss	$$⊢S\subseteq T\to \left(\mathrm{Fun}T\to \mathrm{Fun}S\right)$$
10	4 3 9	sylc	$$⊢\phi \to \mathrm{Fun}S$$
11	1 8 10 5	strfvd	$$⊢\phi \to C=E\left(S\right)$$
12	7 11	eqtr3d	$$⊢\phi \to E\left(T\right)=E\left(S\right)$$