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	|- ( ph -> T e. V )
	strssd.f	|- ( ph -> Fun T )
	strssd.s	|- ( ph -> S C_ T )
	strssd.n	|- ( ph -> <. ( E ` ndx ) , C >. e. S )
Assertion	strssd	|- ( ph -> ( E ` T ) = ( E ` S ) )

Proof

Step	Hyp	Ref	Expression
1		strssd.e	|- E = Slot ( E ` ndx )
2		strssd.t	|- ( ph -> T e. V )
3		strssd.f	|- ( ph -> Fun T )
4		strssd.s	|- ( ph -> S C_ T )
5		strssd.n	|- ( ph -> <. ( E ` ndx ) , C >. e. S )
6	4 5	sseldd	|- ( ph -> <. ( E ` ndx ) , C >. e. T )
7	1 2 3 6	strfvd	|- ( ph -> C = ( E ` T ) )
8	2 4	ssexd	|- ( ph -> S e. _V )
9		funss	|- ( S C_ T -> ( Fun T -> Fun S ) )
10	4 3 9	sylc	|- ( ph -> Fun S )
11	1 8 10 5	strfvd	|- ( ph -> C = ( E ` S ) )
12	7 11	eqtr3d	|- ( ph -> ( E ` T ) = ( E ` S ) )