Axiom ax-hvcom 4985

Description: Vector addition is commutative.

Assertion

Ref	Expression
ax-hvcom	⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → (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 ℋ
3	1, 2	wcel 1092	. . 3 wff A ∈ ℋ
4		cB	. . . 4 class B
5	4, 2	wcel 1092	. . 3 wff B ∈ ℋ
6	3, 5	wa 196	. 2 wff (A ∈ ℋ ∧ B ∈ ℋ )
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 ∈ ℋ ∧ B ∈ ℋ ) → (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