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	$$⊢⟨G,S⟩\in {CVec}_{\mathrm{OLD}}\to \left(G\in \mathrm{V}\wedge S\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-br	$$⊢G{CVec}_{\mathrm{OLD}}S\leftrightarrow ⟨G,S⟩\in {CVec}_{\mathrm{OLD}}$$
2		vcrel	$$⊢\mathrm{Rel}{CVec}_{\mathrm{OLD}}$$
3	2	brrelex12i	$$⊢G{CVec}_{\mathrm{OLD}}S\to \left(G\in \mathrm{V}\wedge S\in \mathrm{V}\right)$$
4	1 3	sylbir	$$⊢⟨G,S⟩\in {CVec}_{\mathrm{OLD}}\to \left(G\in \mathrm{V}\wedge S\in \mathrm{V}\right)$$