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