HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  ax-hvaddid Unicode version

Axiom ax-hvaddid 22543
Description: Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hvaddid

Detailed syntax breakdown of Axiom ax-hvaddid
StepHypRef Expression
1 cA . . 3
2 chil 22458 . . 3
31, 2wcel 1728 . 2
4 c0v 22463 . . . 4
5 cva 22459 . . . 4
61, 4, 5co 6133 . . 3
76, 1wceq 1654 . 2
83, 7wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  hvaddid2  22561  hvpncan  22577  hvsubeq0i  22601  hvsubcan2i  22602  hvsubaddi  22604  hvsub0  22614  hvaddsub4  22616  norm3difi  22685  shsel1  22859  shunssi  22906  omlsilem  22940  pjoc1i  22969  pjchi  22970  spansncvi  23190  5oalem1  23192  5oalem2  23193  3oalem2  23201  pjssmii  23219  hoaddid1i  23325  lnop0  23505  lnopmul  23506  lnfn0i  23581  lnfnmuli  23583  pjclem4  23738  pj3si  23746  hst1h  23766  sumdmdlem  23957
  Copyright terms: Public domain W3C validator