Theorem ressid2

Description: General behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014)

	Ref	Expression
Hypotheses	ressbas.r	|- R = ( W |`s A )
	ressbas.b	|- B = ( Base ` W )
Assertion	ressid2	|- ( ( B C_ A /\ W e. X /\ A e. Y ) -> R = W )

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		iftrue	|- ( B C_ A -> if ( B C_ A , W , ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) ) = W )
5	3 4	sylan9eqr	|- ( ( B C_ A /\ ( W e. X /\ A e. Y ) ) -> R = W )
6	5	3impb	|- ( ( B C_ A /\ W e. X /\ A e. Y ) -> R = W )