Metamath Proof Explorer

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 
|- ( ( F e. T /\ U e. E ) -> <. F , U >. e. ( T X. E ) )

Proof

Step Hyp Ref Expression
1 opelxpi 
 |-  ( ( F e. T /\ U e. E ) -> <. F , U >. e. ( T X. E ) )