Axiom ax-hfvadd 8870

Description: Vector addition is an operation on H~.

Assertion

Ref	Expression
ax-hfvadd	|- +h :(H~ X. H~)-->H~

Detailed syntax breakdown of Axiom ax-hfvadd

Step	Hyp	Ref	Expression
1		chil 8788	. . 3 class H~
2	1, 1	cxp 3168	. 2 class (H~ X. H~)
3		cva 8789	. 2 class +h
4	2, 1, 3	wf 3178	1 wff +h :(H~ X. H~)-->H~

This axiom is referenced by:  hvaddclt 8882  hilabl 9027  hilid 9028  hilvc 9029  hhnv 9032  hhba 9034  hhph 9045  hhssabl 9132  hhssnv 9134  hhshsslem1 9137  hhsssh 9139

Copyright terms: Public domain