Theorem ressbas2

Description: Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	ressbas.r	|- R = ( W |`s A )
	ressbas.b	|- B = ( Base ` W )
Assertion	ressbas2	|- ( A C_ B -> A = ( Base ` R ) )

Proof

Step	Hyp	Ref	Expression
1		ressbas.r	|- R = ( W |`s A )
2		ressbas.b	|- B = ( Base ` W )
3		df-ss	|- ( A C_ B <-> ( A i^i B ) = A )
4	3	biimpi	|- ( A C_ B -> ( A i^i B ) = A )
5	2	fvexi	|- B e. _V
6	5	ssex	|- ( A C_ B -> A e. _V )
7	1 2	ressbas	|- ( A e. _V -> ( A i^i B ) = ( Base ` R ) )
8	6 7	syl	|- ( A C_ B -> ( A i^i B ) = ( Base ` R ) )
9	4 8	eqtr3d	|- ( A C_ B -> A = ( Base ` R ) )