Theorem dvhopclN

Description: Closure of a DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	dvhopclN	⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) → ⟨ 𝐹 , 𝑈 ⟩ ∈ ( 𝑇 × 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		opelxpi	⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) → ⟨ 𝐹 , 𝑈 ⟩ ∈ ( 𝑇 × 𝐸 ) )