Axiom ax-hfvadd 8809

Description: Vector addition is an operation on ℋ.

Assertion

Ref	Expression
ax-hfvadd	⊢ +h :( ℋ × ℋ )–→ ℋ

Detailed syntax breakdown of Axiom ax-hfvadd

Step	Hyp	Ref	Expression
1		chil 8727	. . 3 class ℋ
2	1, 1	cxp 3163	. 2 class ( ℋ × ℋ )
3		cva 8728	. 2 class +h
4	2, 1, 3	wf 3173	1 wff +h :( ℋ × ℋ )–→ ℋ

This axiom is referenced by:  hvaddclt 8821  hilabl 8966  hilid 8967  hilvc 8968  hhnv 8971  hhba 8973  hhph 8984  hhssabl 9071  hhssnv 9073  hhshsslem1 9076  hhsssh 9078

Copyright terms: Public domain