Axiom ax-hfvadd 28777

Description: Vector addition is an operation on ℋ. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-hfvadd	⊢ +ℎ :( ℋ × ℋ)⟶ ℋ

Detailed syntax breakdown of Axiom ax-hfvadd

Step	Hyp	Ref	Expression
1		chba 28696	. . 3 class ℋ
2	1, 1	cxp 5553	. 2 class ( ℋ × ℋ)
3		cva 28697	. 2 class +ℎ
4	2, 1, 3	wf 6351	1 wff +ℎ :( ℋ × ℋ)⟶ ℋ

This axiom is referenced by:  hvaddcl  28789  hilablo  28937  hilid  28938  hilvc  28939  hhnv  28942  hhba  28944  hhph  28955  issh2  28986  hhssabloi  29039  hhssnv  29041  hhshsslem1  29044  hhsssh  29046  shsss  29090  shsel  29091