Axiom ax-hvcom 4985

Description: Vector addition is commutative.

Assertion

Ref	Expression
ax-hvcom	|- ((A e. H~ /\ B e. H~) -> (A +v B) = (B +v A))

Detailed syntax breakdown of Axiom ax-hvcom

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		chil 4958	. . . 4 class H~
3	1, 2	wcel 1092	. . 3 wff A e. H~
4		cB	. . . 4 class B
5	4, 2	wcel 1092	. . 3 wff B e. H~
6	3, 5	wa 196	. 2 wff (A e. H~ /\ B e. H~)
7		cva 4959	. . . 4 class +v
8	1, 4, 7	co 3001	. . 3 class (A +v B)
9	4, 1, 7	co 3001	. . 3 class (B +v A)
10	8, 9	wceq 1091	. 2 wff (A +v B) = (B +v A)
11	6, 10	wi 2	1 wff ((A e. H~ /\ B e. H~) -> (A +v B) = (B +v A))

This axiom is referenced by:  hvcom 5000  hvaddid2t 5003  hvadd23t 5011  hvadd12t 5012  hvsubcan2t 5017  pjpj0 5259  pjpot 5265  shscomt 5284  spanunsn 5482  hoscom 5605  sumdmdi 5785

metamath.org