Theorem resvbas

Description: Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018)

	Ref	Expression
Hypotheses	resvbas.1	|- H = ( G |`v A )
	resvbas.2	|- B = ( Base ` G )
Assertion	resvbas	|- ( A e. V -> B = ( Base ` H ) )

Proof

Step	Hyp	Ref	Expression
1		resvbas.1	|- H = ( G |`v A )
2		resvbas.2	|- B = ( Base ` G )
3		df-base	|- Base = Slot 1
4		1nn	|- 1 e. NN
5		1re	|- 1 e. RR
6		1lt5	|- 1 < 5
7	5 6	ltneii	|- 1 =/= 5
8	1 2 3 4 7	resvlem	|- ( A e. V -> B = ( Base ` H ) )