Theorem ressval2

Description: Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014)

	Ref	Expression
Hypotheses	ressbas.r	|- R = ( W |`s A )
	ressbas.b	|- B = ( Base ` W )
Assertion	ressval2	|- ( ( -. B C_ A /\ W e. X /\ A e. Y ) -> R = ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) )

Proof

Step	Hyp	Ref	Expression
1		ressbas.r	|- R = ( W |`s A )
2		ressbas.b	|- B = ( Base ` W )
3	1 2	ressval	|- ( ( W e. X /\ A e. Y ) -> R = if ( B C_ A , W , ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) ) )
4		iffalse	|- ( -. B C_ A -> if ( B C_ A , W , ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) ) = ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) )
5	3 4	sylan9eqr	|- ( ( -. B C_ A /\ ( W e. X /\ A e. Y ) ) -> R = ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) )
6	5	3impb	|- ( ( -. B C_ A /\ W e. X /\ A e. Y ) -> R = ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) )