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

Axiom ax-hvaddid 23528
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 23443 . . 3
31, 2wcel 1732 . 2
4 c0v 23448 . . . 4
5 cva 23444 . . . 4
61, 4, 5co 6103 . . 3
76, 1wceq 1670 . 2
83, 7wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  hvaddid2  23547  hvpncan  23563  hvsubeq0i  23587  hvsubcan2i  23588  hvsubaddi  23590  hvsub0  23600  hvaddsub4  23602  norm3difi  23671  shsel1  23846  shunssi  23893  omlsilem  23927  pjoc1i  23956  pjchi  23957  spansncvi  24177  5oalem1  24179  5oalem2  24180  3oalem2  24188  pjssmii  24206  hoaddid1i  24312  lnop0  24492  lnopmul  24493  lnfn0i  24568  lnfnmuli  24570  pjclem4  24725  pj3si  24733  hst1h  24753  sumdmdlem  24944
  Copyright terms: Public domain W3C validator