Theorem vcex

Description: The components of a complex vector space are sets. (Contributed by NM, 31-May-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	vcex	⊢ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		df-br	⊢ ( 𝐺 CVecOLD 𝑆 ↔ ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD )
2		vcrel	⊢ Rel CVecOLD
3	2	brrelex12i	⊢ ( 𝐺 CVecOLD 𝑆 → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) )
4	1 3	sylbir	⊢ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) )