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	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	elimnv.5	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
	elimnv.9	⊢ 𝑈 ∈ NrmCVec
Assertion	elimnv	⊢ if ( 𝐴 ∈ 𝑋 , 𝐴 , 𝑍 ) ∈ 𝑋

Proof

Step	Hyp	Ref	Expression
1		elimnv.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		elimnv.5	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
3		elimnv.9	⊢ 𝑈 ∈ NrmCVec
4	1 2	nvzcl	⊢ ( 𝑈 ∈ NrmCVec → 𝑍 ∈ 𝑋 )
5	3 4	ax-mp	⊢ 𝑍 ∈ 𝑋
6	5	elimel	⊢ if ( 𝐴 ∈ 𝑋 , 𝐴 , 𝑍 ) ∈ 𝑋