Theorem elimnv

Description: Hypothesis elimination lemma for normed complex vector spaces to assist weak deduction theorem. (Contributed by NM, 16-May-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	elimnv.1	|- X = ( BaseSet ` U )
	elimnv.5	|- Z = ( 0vec ` U )
	elimnv.9	|- U e. NrmCVec
Assertion	elimnv	|- if ( A e. X , A , Z ) e. X

Proof

Step	Hyp	Ref	Expression
1		elimnv.1	|- X = ( BaseSet ` U )
2		elimnv.5	|- Z = ( 0vec ` U )
3		elimnv.9	|- U e. NrmCVec
4	1 2	nvzcl	|- ( U e. NrmCVec -> Z e. X )
5	3 4	ax-mp	|- Z e. X
6	5	elimel	|- if ( A e. X , A , Z ) e. X